ArghDA M3: Flying-Logic reasoning graph — demote-only verdict propagation

[hyperpolymath]

What & why

The headline capability of the "Flying Logic for provers/solvers" epic, built on the M1 Backend trait (merged #32). A new src/reason/ layer wraps (does not replace) the DAG: the DagDocument is embedded verbatim, and on top go a per-node Verdict, And/Or edge juncts, and a memoised, cycle-safe, demote-only propagation fold.

The honesty invariant (enforced end-to-end)

A node's effective verdict can only be lowered by its dependencies, never manufactured:

• lint-clean + no typecheck = Unknown, never green. Only a real prover exit-0 makes Proven.
• Only Proven is green; Admitted/Postulated are amber.
• Because the fold is demote-only over And import edges, structural amber infects downstream — anything that transitively imports a postulate (or missing-safe / escape-hatch) module is itself capped. Visible before any prover runs.
• Or groups are forgiving (one green route keeps a goal up). Import cycles degrade to Error and terminate. Staleness (closure-hash-changed Proven → Unknown) is applied pre-fold so it propagates. wired marks the CRT-root-reachable cone.

Changes

• src/reason/mod.rs: Junct, ReasonNode (self_verdict/effective/verdict_evidence/soundness/wired), ReasonEdge, ReasonDocument (version:"0.1", embedded dag, crt_roots); the rank/demote/promote lattice; lint→verdict caps; the propagation fold.
• arghda reason <path> [--check]: --check runs the backend per node for real exit-code verdicts; default is structure+lint-derived (all unknown on a clean tree, honestly).
• STATE.a2ml records M3 = 100%.

Verified (ran, not inferred)

• cargo test → 81 passing, 0 failed (61 lib + 20 integration; +9 reason unit tests covering demote / downstream-amber-infection / Or-forgiveness / cycle-termination / wiring / clean-but-unchecked→Unknown, +6 reason integration).
• cargo clippy -D warnings clean · cargo fmt --check clean · check-spdx.sh OK.
• Dogfood — arghda reason tests/fixtures/wellformed --check ran real agda typechecks → the whole cone proven + wired.

A bug dogfooding caught (and I fixed)

The first --check dogfood showed every node wired=false with crt_roots=['tests.fixtures.wellformed.All']. The CLI's discover_roots yields include-root-relative paths, which a stray include_root.join double-prefixed — so the CRT-root ids never matched the node ids. The unit/integration tests missed it because they passed absolute roots (where the join is a silent no-op). Fixed to match the orphan-module rule's convention (paths go straight to module_name_of), plus a regression test that exercises the discover_roots path. Re-dogfooded green.

Next (all unblocked by the stable trait)

M4 Idris2 · M5 SMT (Z3/CVC5) · M2 Cubical-Agda · M3 follow-on (feed real verdicts + staleness from a workspace proven/ state so reason lights the cone without --check).

---

Generated by Claude Code