Surface: fv · Severity: low (latent gate holes; no such shape in-tree today, grep-verified) · Evidence: PoC (regex replay + elaborated attack file, coordinator-reproduced) · Target: f91aa82
Defect (b): the BreaksHash firewall regex (lint_fv_invariants.sh:282) matches only ¬ BreaksHash / Not BreaksHash / BreaksHash → False. axiom breakElim {C : Prop} : BreaksHash → C passes all lints, and from it an UNCONDITIONAL sphincsDigest preimage-equality theorem elaborates — closure [breakElim, propext, Quot.sound, sha256_collision_resistance] — the exact shape the ∨-BreaksHash discipline exists to prevent. Ledger C3 only iterates the 18 pinned closures keys, so a new axiom consumed only by a new unpinned theorem escapes every gate. Live because the tree is routinely edited by LLM agents (the repo's own #14576 note).
Defect (e): the True-typed axiom matcher misses axiom x : (True), : ((True)), and : True → True (paren-wrapping and arrow-to-True conclusions — both provable vacuities wearing an axiom's name).
Fix: extend (b) to any BreaksHash → target and binder forms (h : BreaksHash) in axiom/theorem signatures; in (e), strip parens and take the arrow-chain conclusion before comparing to True; consider an env-wide axiom census (every axiom must be ledger-documented, not only those in pinned closures). Found 2026-08-20 FV red-team.
Surface: fv · Severity: low (latent gate holes; no such shape in-tree today, grep-verified) · Evidence: PoC (regex replay + elaborated attack file, coordinator-reproduced) · Target: f91aa82
Defect (b): the BreaksHash firewall regex (
lint_fv_invariants.sh:282) matches only¬ BreaksHash/Not BreaksHash/BreaksHash → False.axiom breakElim {C : Prop} : BreaksHash → Cpasses all lints, and from it an UNCONDITIONALsphincsDigestpreimage-equality theorem elaborates — closure[breakElim, propext, Quot.sound, sha256_collision_resistance]— the exact shape the ∨-BreaksHash discipline exists to prevent. Ledger C3 only iterates the 18 pinnedclosureskeys, so a new axiom consumed only by a new unpinned theorem escapes every gate. Live because the tree is routinely edited by LLM agents (the repo's own #14576 note).Defect (e): the True-typed axiom matcher misses
axiom x : (True),: ((True)), and: True → True(paren-wrapping and arrow-to-True conclusions — both provable vacuities wearing an axiom's name).Fix: extend (b) to any
BreaksHash →target and binder forms(h : BreaksHash)in axiom/theorem signatures; in (e), strip parens and take the arrow-chain conclusion before comparing toTrue; consider an env-wide axiom census (every axiom must be ledger-documented, not only those in pinned closures). Found 2026-08-20 FV red-team.