From 1de7034d4c5472056b2221f89a65c9a393040c6d Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 9 Aug 2026 11:57:50 -0700 Subject: [PATCH] CLAIMS A1: restore the hypothesis I dropped, and cite the proof that exists Asked whether the six claims match the original theorem, I read formal/THEOREM-LEDGER.json instead of answering from memory, and found three errors in my own claims document. DROPPED HYPOTHESIS. T1 requires side-consistency, the SAME ASSERTION FUNCTION, and the same root set. A1 stated the first and third and omitted the second. Our rewirings preserve sides by construction so no measurement was affected, but dropping a hypothesis from a claim statement is exactly the defect the ledger records against the repository's original T5 -- 'THE HYPOTHESIS MISSING FROM THE REPOSITORY'S T5', which CE-02 proves necessary. The document written to prevent that error committed it, and the correction is kept visible rather than quietly patched. UNDERSTATED EVIDENCE. T1 is proved_compiled: a Lean proof at formal/lean/MinorityProphetCore/Immunity.lean. A1 cited only finite verification. Recorded with the caveat that no Lean toolchain was available here, so proved_compiled is taken from the ledger rather than rebuilt -- a cheap attack for a reviewer with one. MISATTRIBUTED NOVELTY. The ledger already records 116,032 root-preserving forest rewirings with zero violations. reference_mutant_audit.py REPRODUCES that figure; it does not add to it, and A1 now says so. On the question itself: the theorems have shifted from the paper deliberately, and the ledger tracks each shift with its direction and reason -- two flagged narrowed, two generalized. T1 is generalized; the paper restricted which rewirings counted. What drifted without being recorded was my summary, not the theorems. NEW WEAKNESS C6. gate's minority_prophet/__init__.py says 'properties are proven (see FORMAL.md)' and there is no FORMAL.md in that repository. The proofs are real and live here under formal/, so it is a dangling citation rather than a missing proof -- but a reader checking gate's central claim follows a pointer to nothing. Not fixed here: it is a change to another repository. --- CLAIMS.md | 54 ++++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 42 insertions(+), 12 deletions(-) diff --git a/CLAIMS.md b/CLAIMS.md index 83e2c31..a47be9f 100644 --- a/CLAIMS.md +++ b/CLAIMS.md @@ -13,17 +13,39 @@ and those are listed in §B. ## A. Claims -### A1. Theorem 1 (immunity) holds for the reference implementation - -Verdicts are invariant under rewirings that preserve the root set, given -side-consistency on both sides. - -**Evidence.** Exhaustive enumeration to `MAX_CLAIMS_EXHAUSTIVE = 6`: **116,032 -eligible (world, rewiring) pairs, zero violations**, under both the parent-local -and root-based readings. `lineage/reference_mutant_audit.py`, row `correct`. - -**Breaks if.** You exhibit one eligible pair where the verdict changes. The unit -and eligibility rule are stated in that file; you do not have to guess them. +### A1. Theorem 1 (immunity) — machine-checked, and stated with all its hypotheses + +If two worlds are side-consistent, **have the same assertion function**, and have +the same root set, the verdict is identical. No constraint at all is placed on how +the non-root lineage differs. + +**Evidence.** `proof_status: proved_compiled` — a Lean proof at +`formal/lean/MinorityProphetCore/Immunity.lean`, theorem +`MinorityProphet.immunity`. Finite verification recorded in +`formal/THEOREM-LEDGER.json`: 116,032 root-preserving forest rewirings and 1,992 +root-preserving DAG rewirings, zero violations. +`lineage/reference_mutant_audit.py` **reproduces** the 116,032 figure; it does not +add to it. + +**Drift is tracked, not hidden.** The ledger flags T1 `generalized_from_repository: +true` — it is broader than the paper's statement, which restricted which rewirings +counted. Two of the six theorems are flagged narrowed and two generalized, each +with its reason. T5 was narrowed by *adding* the same-assertion hypothesis, which a +counterexample proves necessary. + +**A correction to an earlier draft of this file, kept visible.** A1 previously +omitted the same-assertion hypothesis and cited only the finite verification. Our +rewirings preserve sides by construction, so no measurement was affected — but +dropping a hypothesis from a claim statement is exactly the defect the ledger +records against the repository's original T5. The document meant to prevent that +error committed it. + +**Not verified here.** No Lean toolchain was available in this session, so +`proved_compiled` is taken from the ledger rather than rebuilt. Rebuilding it is a +cheap and worthwhile attack. + +**Breaks if.** The Lean proof does not compile, or you exhibit two worlds meeting +all three hypotheses with different verdicts. ### A2. The immunity ablation is not a test of `root_of` @@ -172,7 +194,15 @@ result is not reproducible without them. It discloses none of their contents. No finding depends on this check — it is a publication guard, not an instrument — but the divergence is real. -**C6. Redaction did not remove anything from history.** Three items redacted on +**C6. Gate cites a proof document that does not exist.** +`minority_prophet/__init__.py` says "properties are proven (see FORMAL.md)". There +is no `FORMAL.md` in the gate repository. The proofs are real and live in this +repository under `formal/`, including the Lean development — so this is a dangling +citation rather than a missing proof, but a reader checking gate's central claim +follows a pointer to nothing. Not fixed here because it is a change to another +repository. + +**C7. Redaction did not remove anything from history.** Three items redacted on 2026-08-09 remain fetchable from earlier commits on the public branch. Removing them means rewriting 292 of 333 commits and breaking all six registration pins, which was judged a worse trade than the exposure (owner decision). The `--sweep`