From 5a221a7e50de30677704b7759ac0b519e94421f6 Mon Sep 17 00:00:00 2001 From: Shay Date: Thu, 11 Jun 2026 13:52:51 -0700 Subject: [PATCH] =?UTF-8?q?docs(epistemic):=20correct=20=C2=A73.4=20promot?= =?UTF-8?q?ion=20doctrine=20+=20de-claim=20enum=20docstring?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit §3.4 said promotion "requires a curator-mediated coherence judgment." That over-states a necessity. ADR-0021 §3 only requires promotion be a function of coherence with the reviewed field. For claims *deductively entailed* by already-COHERENT facts, the entailment proof IS that coherence judgment and can be machine-certified by the sound deductive_logic_v1 engine — the logical arm of the "structural coherence metric" ADR-0021's v2 gap already names. - position_paper.md §3.4: split "own asserted output" (no standing — kept) from "deductively entailed from COHERENT facts" (proof = coherence judgment); relocate review to the *reading*, not the deduction; flag the proof-carrying path as specified-but-unwired with a link to the new issue. - teaching/epistemic.py: the EpistemicStatus docstring claimed transitions are "computed from coherence" — they are not; review_correction carries status as a curator-supplied input. Docstring now states this honestly. - docs/issues/proof-carrying-coherence-promotion.md: thorough spec for the unbuilt capability (scope, the reading hazard, INV-21 impact, trust boundary, falsification tests, phased plan, proposed ADR-0218). No runtime behavior change. Green: test_epistemic_invariants, test_epistemic_phase3_state_tagging, TestINV21OneMutationPath (15 passed). --- .../proof-carrying-coherence-promotion.md | 226 ++++++++++++++++++ docs/position_paper.md | 35 ++- teaching/epistemic.py | 16 +- 3 files changed, 267 insertions(+), 10 deletions(-) create mode 100644 docs/issues/proof-carrying-coherence-promotion.md diff --git a/docs/issues/proof-carrying-coherence-promotion.md b/docs/issues/proof-carrying-coherence-promotion.md new file mode 100644 index 00000000..2b5c530a --- /dev/null +++ b/docs/issues/proof-carrying-coherence-promotion.md @@ -0,0 +1,226 @@ +# Issue — Proof-carrying coherence promotion (the logical arm of ADR-0021's v2 gap) + +**Status:** Open — specification only, no code authorized +**Raised:** 2026-06-11 +**Surface:** `teaching/epistemic.py`, `teaching/review.py`, the deductive +engine (`deductive_logic_v1`), `vault/store.py`, INV-21 one-mutation-path +**Governing ADR:** [ADR-0021 — Epistemic Grade Policy](../decisions/ADR-0021-epistemic-grade-policy.md) +(this issue specifies one arm of that ADR's *"Named gap (v2 work, explicit)"*) +**Requires before any code:** a ratified ADR (provisional **ADR-0218**, number +to be confirmed against in-flight branches — current max committed is ADR-0217) + +--- + +## TL;DR + +The position paper §3.4 and the `EpistemicStatus` docstring both implied a +stronger promotion story than the code delivers. Two things were corrected in +the same change that raised this issue: + +1. **Doctrine precision (paper §3.4).** "Promotion requires a *curator-mediated* + coherence judgment" over-states a *necessity*. The doctrine (ADR-0021 §3) only + requires that promotion be a function of **coherence with the reviewed field**. + For the subclass of claims that are *deductively entailed* by already-`COHERENT` + facts, the entailment proof **is** that coherence judgment and can be + machine-certified by CORE's sound deductive engine — no human re-deciding + settled logic. +2. **Code honesty (`teaching/epistemic.py`).** The enum docstring claimed + transitions are *"computed from coherence with the existing reviewed field."* + They are not computed; `review_correction` carries the status as a + curator-supplied input. The docstring now says so. + +**This issue specifies the missing capability**: a *proof-carrying promotion* +path that lets a `SPECULATIVE` claim become `COHERENT` **iff** it is deductively +entailed by an already-`COHERENT` premise set, with the proof chain as the audit +artifact. It is **designed-but-unwired**. Building it touches the single most +protected boundary in the system (INV-21), so it is ADR-gated. + +--- + +## 1. Context — what is true today + +| Claim | Reality in code | +|---|---| +| "Coherence is the only admission signal." | True and load-bearing (ADR-0021 §3). Source/credentials/own-output carry no standing. | +| "Transitions are computed from coherence." | **False today.** `teaching/review.py::review_correction` checks identity-override + emptiness, then sets `outcome`; `epistemic_status` is a **passed-in parameter** (default `SPECULATIVE`). No coherence computation runs. | +| "A sound deductive engine exists." | True. `deductive_logic_v1` is sound + complete for propositional entailment, ROBDD-canonical (ADR-0201/0202), independently oracle-checked, holdout wrong=0, SHA-pinned. | +| "The engine certifies promotions." | **False today.** The deductive engine and the binding-graph proof DAG (ADR-0132–0135) have **zero consumers** in the teaching/promotion path. | +| "Only one path writes the reviewed field." | True (INV-21). Every vault writer is allowlisted in `tests/test_architectural_invariants.py::TestINV21OneMutationPath`. | + +ADR-0021 already anticipated this exact gap. Its *"Named gap (v2 work, +explicit)"* says v1 is "honest about the gap: … the coherence judgment behind a +tag is still curator-mediated, and the architecture commits to closing that gap +on a stated path." Its v2 sketch is **geometric** (`cga_inner(claim, field) ≥ +τ`). This issue is the **logical** complement to that sketch. + +## 2. Two arms of one goal — do not conflate them + +ADR-0021's "structural coherence metric" successor to curator mediation has two +distinct mechanizations, and they catch different failures: + +- **Geometric arm (ADR-0021 v2 sketch).** `cga_inner(claim_versor, field) ≥ + τ_admit` and no reviewed relation with `cga_inner ≤ τ_reject`. Detects + *contradiction with / proximity to* the reviewed field. Metric, continuous, + threshold-tuned. +- **Logical arm (this issue).** The claim is *deductively entailed* by a + `COHERENT` premise set, certified by the sound engine. Detects + *derivability from* the reviewed field. Combinatorial, exact, no threshold. + +These are complementary, **not** substitutes. The field metric does not perform +entailment — logic is combinatorial, not metric. A claim can sit far from any +existing versor (low geometric agreement) yet be a rigorous deductive +consequence of reviewed premises, and vice-versa. The logical arm is the one the +already-built engine can deliver soonest, because the deductive engine already +exists and is wrong=0; it just is not wired to the promotion path. + +## 3. Scope — what proof-carrying promotion IS and IS NOT + +**IS:** +- A path that promotes `SPECULATIVE → COHERENT` **only** when a sound proof + derives the claim from an exclusively-`COHERENT` premise set. +- Proof-carrying: the promotion artifact embeds the proof chain (binding-graph + DAG / ROBDD witness) so replay can re-verify it deterministically. +- Audit-first: the proof is the justification; no source, credential, or + confidence score appears anywhere in the decision. + +**IS NOT:** +- Not promotion of the system's own *asserted* output (a generated surface, a + guess). That remains forbidden — promoting it and re-feeding it is the + fabrication loop ADR-0021 and CLAUDE.md exist to prevent. +- Not a source-trust fast-path. "Came from a trusted place" never promotes + anything. INV-21's prohibition on "a fast-path for known-good sources" stands. +- Not a relaxation of `wrong=0`. It adds a *narrower* admission, gated by a + sound proof, not a *looser* one. +- Not the geometric arm. That is separate ADR-0021 v2 work. + +## 4. The crux — the reading hazard, not the deduction + +The deduction is mechanical and already wrong=0. **The fallible step is the +reading**, and the design must put the whole defensive burden there: + +1. **Translation faithfulness.** Natural-language claim → propositional / + binding-graph form. A sound proof over a *misread* premise is a sound proof of + the wrong thing. This is the live `wrong=0` hazard surface (the self-check is + *soundness*, not *correctness* — there is no gold to compare against). +2. **Premise grounding.** Every premise fed to the engine must *already* be + `COHERENT` in the vault — verified by status, not assumed. A premise that is + `SPECULATIVE`/`CONTESTED` must make the proof inadmissible for promotion. +3. **Premise selection / closure.** The premise set must be explicit and + bounded; the proof must not silently pull in unreviewed facts. + +**Design consequence:** proof-carrying promotion does **not** remove human +review — it *relocates* it. The human (or a separately-ratified structural +check) certifies the **reading** (1–3); the engine certifies the **entailment**. +The autonomy is only ever as safe as the faithfulness of the reading, and the +design must make an unfaithful reading *fail closed* (refuse to promote), never +fall through to admission. This mirrors why today's `idle_tick` continuous- +learning loop is proposal-only → pending-HITL even for *determined* facts. + +## 5. Where it touches the architecture + +- **INV-21 one-mutation-path (highest risk).** Promotion writes the reviewed + field. Any new promoter must be added to the `TestINV21OneMutationPath` + allowlist *with documented justification*, or — preferably — routed through the + existing reviewed write path so no new mutation site is created. The CI failure + is the prompt, not a thing to route around. A proof-carrying promoter that + bypasses the single path silently re-introduces the backdoor the invariant + forbids. +- **`teaching/review.py`.** Either `review_correction` gains an + entailment-certification branch, or a sibling reviewed-path function is added + that consumes a proof artifact. Must not become a *parallel* learning path + (CLAUDE.md: "Do not create a parallel correction/learning path"). +- **`teaching/epistemic.py`.** No enum change needed; `COHERENT` already is the + target. The transition *function* is what gains a sound-proof input. +- **Deductive engine (`deductive_logic_v1`) + binding-graph DAG (ADR-0132–0135, + ROBDD ADR-0201/0202).** First real consumer of the proof_chain substrate. + proof_chain Phase 2 (binding-graph wiring, acyclicity refusal, modus_ponens) + is a prerequisite — today only `transitive` (ADR-0083) actually executes. +- **`vault/store.py`.** Reads premise `epistemic_status`; the promoter must query + `min_status=COHERENT` for premises and refuse if any premise is not admissible. +- **`core/cognition/trace.py`.** The proof artifact and resulting status fold + into `trace_hash` (ADR-0021 §Schema impact already requires status in the + hash). Replay must re-verify the proof bit-for-bit. + +## 6. Trust boundary statement (required by CLAUDE.md) + +Proof-carrying promotion consumes (a) a premise set drawn from the vault and (b) +a reading of a candidate claim into propositional form. The **untrusted** input +is the *reading* (it may originate from user text or a model-style proposer). The +boundary rule: **the reading is data, never authority.** The promoter must: + +- Refuse promotion unless every premise resolves to a stored `COHERENT` entry. +- Refuse promotion unless the proof is produced by the pinned sound engine and + re-verifies on replay. +- Never let a proposer-supplied "proof", "status", or "confidence" field + influence the decision (echo-and-ignore, as the epistemic-truth-state demo + does for `proposed_state`). +- Fail closed: any unresolved premise, any reading ambiguity, any engine refusal + → no promotion, claim stays `SPECULATIVE`. + +## 7. Falsification / test obligations + +Per CLAUDE.md *"Schema-Defined Proof Obligations"* — every claimed guarantee +must have a test that **fails loudly** when the guarantee is violated. A test +that passes under a broken implementation is decoration. Required failing-tests: + +1. **Entailed-from-COHERENT promotes.** A claim genuinely entailed by `COHERENT` + premises is promoted, and the proof artifact re-verifies on replay. +2. **Non-entailed does NOT promote.** A claim merely *consistent* with (but not + entailed by) the field stays `SPECULATIVE`. Mutating the proof to a + non-sequitur must flip the test red. +3. **Premise-status gate.** If any premise is `SPECULATIVE`/`CONTESTED`/ + `FALSIFIED`, promotion is refused. Silently downgrading the premise check must + make this test fail. +4. **Reading-hazard fail-closed.** A deliberately misread premise (right symbols, + wrong proposition) must NOT promote — the reading certification must catch it. +5. **No proposer authority.** A proposer-supplied proof/status/confidence field + is ignored; promotion decision is byte-identical with and without it. +6. **INV-21 intact.** The one-mutation-path allowlist test still passes; if a new + write site was added, its justification is present and the test references it. +7. **Determinism.** Double-run promotion is byte-identical; `trace_hash` includes + the proof; replay re-verifies. +8. **wrong=0 preserved.** The full serving + deductive holdout lanes stay + wrong=0 after the path is wired. + +## 8. Phased plan + +- **P0 — Doc + honesty (this change, no feature).** Paper §3.4 corrected; enum + docstring de-claimed; this issue written. ✅ +- **P1 — Reading contract (spec).** Define the NL→proposition reading contract + and its certification surface (what makes a reading "faithful enough" to gate + on). This is the hard, hazard-bearing part; it gets its own design pass and may + itself stay curator-mediated initially. +- **P2 — proof_chain Phase 2 prerequisite.** Wire the binding-graph DAG as the + first consumer (acyclicity refusal, modus_ponens) so a proof artifact exists in + a replayable form. (Already a deferred item; this issue is a forcing function.) +- **P3 — Proof-carrying promoter (behind ADR-0218).** Add the + entailment-certification branch to the *single* reviewed write path. Premise + status gate + fail-closed reading gate + proof-in-trace. All §7 tests green. +- **P4 — Geometric arm (separate, ADR-0021 v2).** Out of scope here; tracked so + the two arms are not conflated. + +## 9. Proposed ADR-0218 must rule on + +- Whether proof-carrying promotion extends the existing reviewed path or is + allowlisted as a new INV-21 write site (strong preference: extend, don't add). +- The reading-certification bar for P1 (curator-certified reading vs. a + structural reading check) and whether P3 ships with reading still + curator-mediated (entailment automated, reading human) as the honest first cut. +- The exact admissibility predicate: premises ⊆ `COHERENT`, proof from pinned + engine, replay re-verifies, fail-closed on any gap. +- Trace-hash composition for the proof artifact. + +## 10. Explicit non-goals + +- Geometric coherence admission (`cga_inner ≥ τ`) — ADR-0021 v2, separate. +- Promotion of generated/asserted output — permanently forbidden. +- Any source-authority or confidence-weighted promotion — permanently forbidden. +- Relaxing `wrong=0` or the non-hardening invariant — out of question. + +## 11. Acceptance criteria for closing this issue + +This issue is closed when **either** (a) ADR-0218 is ratified and P3 lands with +all §7 tests green and wrong=0 preserved, **or** (b) the architect rules the +logical arm is not worth wiring and records that decision — in which case paper +§3.4 must be amended again to drop the "specified but not yet wired" forward +reference and state plainly that promotion is curator-mediated by design. diff --git a/docs/position_paper.md b/docs/position_paper.md index 3191b700..c70b193c 100644 --- a/docs/position_paper.md +++ b/docs/position_paper.md @@ -131,15 +131,36 @@ probabilistic suggestion. Knowledge enters the runtime field through one path: the reviewed teaching loop. Every new correction enters at `EpistemicStatus.SPECULATIVE`. Promotion to `COHERENT` — the only status admissible as evidence in downstream inference — -requires a curator-mediated coherence judgment against the existing reviewed -field. Source authority, institutional credentials, and the system's own prior -output have no standing. Only coherence with reviewed claims counts. +requires a **coherence judgment** against the existing reviewed field. The +admission signal is coherence and only coherence: source authority, institutional +credentials, and the system's own *asserted* output carry no standing. Provenance +is retained for audit and revision, never as a promotion signal. + +That judgment is curator-mediated today, and for most corrections it must be. The +fallible step is not the logic but the *reading* — translating a natural-language +claim into the field's propositional form, and selecting which reviewed facts it +bears on. A sound inference over a misread premise is a sound proof of the wrong +thing, so a human certifies the reading before a correction enters the reviewed +structure. + +One subclass is different in principle. A claim that is *deductively entailed* by +facts already marked `COHERENT` is not new information and is not the system's own +opinion — it makes explicit what the reviewed field already contains. For that +subclass the entailment proof *is* the coherence judgment, and CORE's sound, +independently-checked deductive engine (`deductive_logic_v1`, §4) can certify it +deterministically, with the proof chain as the audit artifact — the logical form +of the *"structural coherence metric"* ADR-0021 names as the successor to curator +mediation. What review still gates there is the faithfulness of the reading, not +the deduction. This proof-carrying promotion path is **specified but not yet +wired** (see +[`docs/issues/proof-carrying-coherence-promotion.md`](issues/proof-carrying-coherence-promotion.md)); +until it lands, all promotion is curator-mediated. This is not a safety overlay. It is a consequence of the decoding thesis: if the -system decodes a reality that already is, then inputs that contradict reviewed -structure need review before they enter that structure. A system that accepts any -confident-sounding correction without review is a generative system in different -clothing. +system decodes a reality that already is, then inputs that contradict — or merely +fail to follow from — reviewed structure need review before they enter that +structure. A system that accepts any confident-sounding correction without review +is a generative system in different clothing. Two invariants enforce this at the architecture level, not the policy level. diff --git a/teaching/epistemic.py b/teaching/epistemic.py index 37b26313..8fe3b8e1 100644 --- a/teaching/epistemic.py +++ b/teaching/epistemic.py @@ -20,9 +20,19 @@ from enum import Enum, unique class EpistemicStatus(Enum): """Position of a claim in the reviewed revision graph. - Coherence is the only admission signal (ADR-0021 §3). Transitions - between statuses are *computed from coherence with the existing - reviewed field*, not asserted by source authority. + Coherence is the only admission signal (ADR-0021 §3): a status is a + function of coherence with the existing reviewed field, never of + source authority, credentials, or the system's own asserted output. + + The *judgment behind* a transition is curator-mediated today — + ``review_correction`` carries the resulting status as an input, it does + not yet compute it. ADR-0021's "Named gap (v2 work)" commits to + replacing curator mediation with a structural coherence metric; one + arm of that successor (proof-carrying promotion for the deductively + *entailed* subclass, via the sound ``deductive_logic_v1`` engine) is + specified but not yet wired — see + ``docs/issues/proof-carrying-coherence-promotion.md``. Until it lands, + do not read this enum as evidence of an automated coherence computation. """ COHERENT = "coherent"