Surface: fv · Severity: low (honesty, not soundness) · Evidence: PoC (elaborated Lean proof, coordinator-reproduced) · Target: f91aa82
Claimed: THE_CLAIM.md:232 + Theorems.lean:338 — "theft_free's genuine 9 premises … A2 + A3.1 + A5(×4) + kernel"; proof_mutations.json's A2 entry claims ledger_claim: "a genuine SEMANTIC premise" (the ledger doesn't say that).
Defect (V2 confirmed): A2's exact statement re-proves from the handleOp definition with kernel-only closure:
'entrypoint_honest_proved' depends on axioms: [propext, Classical.choice, Quot.sound]
Per the playbook's V2 rule a kernel-re-provable axiom carries zero information. The mutation gate's "A2-load-bearing" test can't distinguish "load-bearing" from "mentioned" (a rename breaks the build either way). Docs already half-admit this ("Lean fiction"; "could be restated as a theorem") — the premise-count marketing is what's left.
Fix: demote A2 to a theorem (proof exists, ~10 lines — /tmp/redteam/rt26/a2_tautology8.lean from the red-team pass), re-pin THEFT_EXPECTED 11→10 names + the C16/closure ledger entries; or reword the "genuine premises" claims. Demotion shrinks the advertised trust base by one — a strict honesty improvement; the c.2 tripwire goes red until re-pinned (expected, not a regression). Found 2026-08-20 FV red-team.
Surface: fv · Severity: low (honesty, not soundness) · Evidence: PoC (elaborated Lean proof, coordinator-reproduced) · Target: f91aa82
Claimed:
THE_CLAIM.md:232+Theorems.lean:338— "theft_free's genuine 9 premises … A2 + A3.1 + A5(×4) + kernel";proof_mutations.json's A2 entry claimsledger_claim: "a genuine SEMANTIC premise"(the ledger doesn't say that).Defect (V2 confirmed): A2's exact statement re-proves from the
handleOpdefinition with kernel-only closure:Per the playbook's V2 rule a kernel-re-provable axiom carries zero information. The mutation gate's "A2-load-bearing" test can't distinguish "load-bearing" from "mentioned" (a rename breaks the build either way). Docs already half-admit this ("Lean fiction"; "could be restated as a theorem") — the premise-count marketing is what's left.
Fix: demote A2 to a
theorem(proof exists, ~10 lines —/tmp/redteam/rt26/a2_tautology8.leanfrom the red-team pass), re-pinTHEFT_EXPECTED11→10 names + the C16/closure ledger entries; or reword the "genuine premises" claims. Demotion shrinks the advertised trust base by one — a strict honesty improvement; the c.2 tripwire goes red until re-pinned (expected, not a regression). Found 2026-08-20 FV red-team.