gap2SignatureBlockerAttackStatus_flags
plain-language theorem explainer
Status snapshot for the Gap-2 signature-blocker attack: Burnside mass packaging, fiberwise amplitude, cube mass at shell 2, and blocker reformulation have landed; the signature blocker, eventual balance impossibility, and continuum-and-measure flip have not; asymptotic single-signature concentration is flagged as failing. Anyone auditing the Seven Gaps gravity ledger cites this for the honest terminal state of Wave C1 R4. Proof is a one-line decidability check on the concrete status record.
Claim. The Gap-2 signature-blocker attack status asserts: Burnside signature-mass packaging has landed; amplitude fiberwise decomposition has landed; cube mass at shell $2$ has landed; blocker reformulation has landed; the signature blocker itself is not proved; eventual fiber-mass balance impossibility is not proved; asymptotic single-signature concentration fails; and the Gap-2 continuum-and-measure claim remains false.
background
This module is the Wave C1 R4 terminal attack on the Fin-8 oscillatory tail blocker in the Seven Gaps gravity program. The target Prop would obstruct large-shell cancellation by a single dominant signature mass. Under the banked Burnside identity, signature mass of a triple $(v,e,t)$ equals the cardinality of the exact complex divided by $v!,e!,t!$. Shell mass is the sum of signature masses over the shell.
The module packages signatureMass/burnsideMass with equality via the banked class-measure sum, shell-mass decomposition, sigmaTick packaging of shell-signature ticks, and a Burnside-weighted fiberwise exact-shell amplitude. External enumeration shows the cube signature $(n,n,n)$ dominates only mesoscopically (roughly $n\lesssim 200$); by $n\approx 400$ the top piece is below $1/8$ of shell mass, so uniform asymptotic concentration and the $>1/8$ balance-impossibility route both fail.
The status structure is a concrete Boolean record of what landed versus what remains open. This theorem simply freezes that record as a proved conjunction.
proof idea
One-line decidability proof. The status definition hard-codes eight Boolean fields; decide discharges the eight equalities to true/false by computation on those literals. No lemmas beyond the status def itself are invoked.
why it matters
Honest terminal ledger entry for the Gap-2 signature-blocker attack. It records that reduction infrastructure (Burnside mass, fiberwise amplitude, shell-2 cube mass, blocker reformulation as an explicit sequence Prop) is theorem-grade, while the blocker Prop itself, eventual balance impossibility, and the Gap-2 continuum-and-measure flip are not proved. It also locks in the diagnosis that asymptotic single-signature concentration fails, so routes (a)/(b)/(c) are closed as uniform strategies. Downstream consumers of the Seven Gaps gravity chain can cite this rather than re-audit the module. No parent theorems yet (used_by empty); the value is audit transparency inside the gravity domain, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.