core/docs/decisions/ADR-0204-proof-graph-builder.md

ADR-0204 — Proof-Graph Builder (proof_chain's first binding-graph consumer)

Status: Accepted (proof_chain phase 2.2 — structure only; ADR-0201 §Deferred) Date: 2026-06-02 Relates to: ADR-0132 (binding-graph data model — the substrate this consumes), ADR-0201 / ADR-0201.1 (canonicalizer + out-of-regime detector), ADR-0202 (proposition representation contract), ADR-0203 (acyclicity guard this exercises). Deferred to: ADR-0205 (modus_ponens + disagreement rule), ADR-0206 (atom→carrier grounding).

---

Context

The ADR-0132 binding graph is the proof-DAG substrate; until now it had zero consumers. Phase 2.2 makes proof_chain its first: a builder that translates a propositional proof into a SemanticSymbolicBindingGraph. Structure only — no inference rule (modus_ponens is 2.3). The builder constructs the DAG and lets the substrate's guards fire; it asserts nothing about whether a step is valid.

Decision

One canonical proof input shape

generate/proof_chain/model.py defines the single committed proof representation — the corpus surface shapes desugar onto it, so proof input never becomes a second dialect (the ADR-0202 discipline, for proofs):

• ProofNode(node_id, formula, depends_on, rule) — node_id is a Python identifier (→ symbol_id); formula is an ADR-0202 propositional string; depends_on names derived-from nodes; rule is the inference label.
• Proof(nodes, conclusion_id).
• proof_from_premises(premises, conclusion, rule) desugars the premises/conclusion/rule corpus shape (each premise → a rule="premise" node; the conclusion → one node depending on all premises).

The mapping (every node → one symbol + one equation)

ProofNode	Binding-graph target
node_id	SymbolBinding.symbol_id / BoundEquation.lhs_symbol_id
canonicalize(formula).canonical_key	BoundEquation.rhs_canonical
depends_on	BoundEquation.dependencies
rule	BoundEquation.operation_kind ("premise" for assumptions)

Premises are equations with empty dependencies and operation_kind="premise" — uniform, and every node thereby carries its proposition's canonical key in rhs_canonical (which 2.3's rule check needs). Construction runs the ADR-0203 acyclicity guard + ADR-0132 referential integrity in __post_init__: a cyclic or dangling proof refuses there, through the real builder path.

Admissibility-dispatch confirmation (the operation_kind question)

The builder writes logic labels ("premise", later "modus_ponens") into operation_kind, a field the math admissibility checker reads (closed arithmetic vocab). Confirmed by code + test that the dispatch handles unknown-to-math kinds gracefully and never misroutes: check_admissibility ends in raise AdmissibilityError("unknown_operation", kind) — there is no default into _check_additive. Empirically, on built proof equations: a premise (no deps) reaches the dispatch → unknown_operation; a modus_ponens (unitless deps) refuses at unit-resolution → unit_unbound. Neither returns a math UnitProof; neither misroutes. Baked into test_proof_operation_kinds_refuse_in_admissibility_never_misroute.

Named constraint carried to 2.3: check_admissibility runs _resolve_dep_units before the kind dispatch, so a proof equation with dependencies refuses with unit_unbound first. The 2.3 modus_ponens check must therefore be wired to bypass unit resolution (dispatch-on-kind before _resolve_dep_units, or a separate proof-admissibility entry) — proofs have no units to resolve.

Open items (named for 2.3, not "we'll see")

1. Conclusion typing. 2.2 tracks ProofGraph.conclusion_symbol_id (not a BoundUnknown — ADR-0135's question_form vocab does not fit "is this proven"). The 2.3 disagreement rule operates on the conclusion's canonical key and may need richer conclusion typing; revisit conclusion typing in ADR-0205.
2. semantic_role for propositions. Proposition symbols use semantic_role="unknown" because the closed ADR-0132 role vocab (entity/quantity/rate/…) has no "proposition" member. This is the role-field analog of the operation_kind situation. Extending SEMANTIC_ROLES would be an ADR-0132 closed-vocab change (its exact set is test-pinned); left as "unknown" for the additive 2.2 builder. Decide whether to add a "proposition" role when proofs become load-bearing.
3. unit_proof. Set to the PROOF_NO_UNIT sentinel — units are non-applicable to propositional proof steps. Composes with constraint (2) above for 2.3's admissibility wiring.

Honesty boundary (load-bearing — every phase-2 ADR, 0203–0205)

Through phase 2.3, proof_chain is sound over its declared atoms, not grounded in recognized input (grounding is 2.4 / ADR-0206). The builder is structure-only: it builds and refuses cycles/malformed/out-of-regime formulas; it makes no soundness or grounding claim. Out-of-regime node formulas inherit the canonicalizer's typed LogicRegimeError refusal (no silent predicate-logic admission).

Evidence

• tests/test_proof_chain_builder.py — 9 tests: valid DAG (incl. PC-MP-001 desugared) + multistep DAG construct; PC-CYCLE-001 refuses through the real builder (circular_dependency); canonical_key round-trips byte-identical + equivalent node formulas share rhs_canonical; admissibility-dispatch confirmation; self/dangling-dependency refusals; out-of-regime node formula refuses.
• Mutation-verified: neutering the depends_on → dependencies wiring makes PC-CYCLE-001 construct without refusal → the cycle test fails. The dep-wiring is load-bearing, not the guard alone.
• First-consumer non-perturbation: full binding-graph + admissibility surface green (the 392 intact); builder is purely additive (touches no math path).
• Real corpus fixture: PC-CYCLE-001 refuses through the builder; PC-MP-001/002/003 structures construct (rule-check deferred to 2.3). Smoke: 67 passed.

Deferred

• 2.3 — modus_ponens (_check_modus_ponens via ROBDD equivalence, wired to bypass unit-resolution per §named constraint) + the disagreement/uniqueness rule (the wrong=0 mechanism) — ADR-0205.
• 2.4 — atom→ADR-0144 EpistemicNode grounding — ADR-0206.