CLAIMS A1: restore the hypothesis I dropped, and cite the proof that exists

[Silentpartnercoding]

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.

1. 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 REPOSITORYS T5", which CE-02 proves is necessary.

The document written to prevent that error committed it. The correction is kept visible rather than quietly patched.

2. Understated evidence

T1 is proved_compiled — a Lean proof at formal/lean/MinorityProphetCore/Immunity.lean. A1 cited only finite verification. Now recorded, with the caveat that no Lean toolchain was available in this session, so proved_compiled is taken from the ledger rather than rebuilt. A cheap attack for a reviewer who has one.

3. Misattributed novelty

The ledger already records 116,032 root-preserving forest rewirings, 0 violations. reference_mutant_audit.py reproduces that figure — it does not add to it. A1 now says so.

On the question that prompted this

The theorems have shifted from the paper, deliberately, and the ledger tracks every shift with direction and reason — two flagged narrowed_from_repository, two generalized_from_repository. T1 is generalized: the paper restricted which rewirings counted.

What drifted without being recorded was my summary, not the theorems.

New weakness: C6

gate/minority_prophet/__init__.py says "properties are proven (see FORMAL.md)" — and there is no FORMAL.md in gate. 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.