4cae904563
Phase 2.2, structure only (no inference rule — modus_ponens is 2.3). Translates a Proof into a SemanticSymbolicBindingGraph; the ADR-0203 acyclicity guard + ADR-0132 referential integrity fire at construction. - generate/proof_chain/model.py: the one canonical proof input shape (ProofNode/Proof + proof_from_premises desugaring of the corpus premises/conclusion shape). - generate/proof_chain/builder.py: build_proof_graph — node→symbol+equation; canonical_key→rhs_canonical, depends_on→dependencies, rule→operation_kind; premises = empty-deps/op="premise"; unit_proof=PROOF_NO_UNIT, admissibility="pending"; conclusion tracked as conclusion_symbol_id. - tests: 9 — valid DAG (PC-MP-001 desugared) + multistep construct; PC-CYCLE-001 refuses THROUGH the real builder (circular_dependency); canonical_key round-trips byte-identical + equivalent formulas share rhs_canonical; admissibility-dispatch confirmation; self/dangling refusals; out-of-regime node refuses. Mutation-verified (drop dep-wiring -> cycle admitted -> test fails). Admissibility dispatch confirmed graceful on proof operation_kinds: unknown kinds -> AdmissibilityError(unknown_operation), unitless deps -> unit_unbound; NEVER misroutes into _check_additive. Named 2.3 constraint: check_admissibility runs _resolve_dep_units before dispatch, so modus_ponens must bypass unit-resolution. Open items named for 2.3 (ADR-0204): conclusion typing (BoundUnknown revisit), semantic_role="unknown" (closed vocab has no "proposition"), unit_proof sentinel. Additive (first consumer; math lane untouched). Full binding-graph surface green; smoke 67. Honesty boundary: through 2.3, sound over declared atoms, not grounded in input.
117 lines
6.3 KiB
Markdown
117 lines
6.3 KiB
Markdown
# 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.
|