torusClassMassStatus_flags
plain-language theorem explainer
Records the Crux-2 consistency-gate scorecard for torus class mass under quotient bookkeeping: five labeled/class identities are marked proved and four absolute-suppression or continuum claims remain false. Gravity auditors cite it to lock what this module does and does not claim after the C6 wording repair. The proof is nine reflexivity checks against the status record.
Claim. The torus class-mass status record asserts: labeled member masses are bounded; labeled summands are bounded; labeled summands tend to zero; the class-mass identity is proved; the fiber-cardinality bound on class mass is proved; and the following remain unproved: absolute suppression of pushforward class mass, the $Z_{\mathrm{RS}}$ continuum limit, derivation of the substrate measure, and the Gap-1 bridge.
background
This module sits in the Seven Gaps gravity stack as the Crux-2 consistency gate for the canonical torus under protocol QUOTIENT_BOOKKEEPING. The panel's C6 trap forbade the ill-posed claim that the pushforward class summand is suppressed as $N^{-3}$: pushforward class mass equals $|\mathrm{fiber}|\cdot\mu(T_N)$, and fiber cardinality grows with the labeled class.
The honest split keeps two objects separate. On the labeled side one has $\mu(K)\le 1/N^3$ for every labeled member of the torus class, the unit-modulus labeled summand bound $|\mu(K)\cdot z|\le 1/N^3$, and the corresponding $N\to\infty$ tendsto-zero statements. On the class side one has the identity $\mathrm{classMass}([T_N])=|\mathrm{fiber}|\cdot\mu(T_N)$ and the bound $\mathrm{classMass}([T_N])\le|\mathrm{fiber}|/N^3$, without any absolute $N^{-3}$ claim.
The upstream definition torusClassMassStatus is the concrete status record whose Boolean fields this theorem freezes: five trues for the proved labeled/class facts, four falses for the forbidden or still-open continuum and bridge claims.
proof idea
One-line term proof: the nine conjuncts are definitional equalities against the field values of torusClassMassStatus, discharged by nine rfl steps packed as a single tuple constructor. No lemmas are applied; the theorem is a machine-checkable freeze of the status record.
why it matters
Inside Recognition Science gravity, Seven Gaps needs an auditable gate that separates what is proved about the Freudenthal torus from what the kill list forbids. This flag theorem is that gate: it certifies the labeled $\mu\le N^{-3}$ and labeled-summand tendsto-zero facts, plus the honest fiber-card class-mass identity and bound, while explicitly leaving false the absolute pushforward suppression, $Z_{\mathrm{RS}}$ continuum limit, substrate-measure derivation, and Gap-1 bridge.
No downstream consumers are wired yet (used_by is empty), so the declaration functions as a panel-facing scoreboard rather than a lemma in a larger proof. It closes the wording-repair obligation for Crux-2 under QUOTIENT_BOOKKEEPING and documents which continuum and bridge questions remain open scaffolding outside this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.