ClassPushforwardStatus
plain-language theorem explainer
Status record for the Seven Gaps class-pushforward wave: boolean flags that mark which path-sum bookkeeping facts are closed in this module and which remain red. Gravity auditors cite it to read the honest progress board for Crux-2 (quotient bookkeeping of Z). It is a pure structure definition; the companion value fills each flag by rfl.
Claim. A status record whose fields are booleans recording: whether the generic finite-sum fiber decomposition over a quotient is proved; whether class mass is defined; whether the labeled path-sum $Z$ equals the class-pushforward sum; whether class mass equals fiber cardinality times $\mu$; whether a non-singleton fiber is exhibited; and whether several further claims hold (that $Z$ is the inequivalent-class sum with $1/|\mathrm{Aut}|$ weights; that a quotient-first object is constructed; continuum limit of $Z_{\mathrm{RS}}$; substrate measure derived; gap-1 bridge derived). The last five are documented as false or red in this wave.
background
Module setting is Seven Gaps Crux-2 (pillar 2, path-sum): the class pushforward of the labeled path-sum $Z$, under the locked protocol QUOTIENT_BOOKKEEPING. For a finite type with a setoid, the sum of an additive function over labeled complexes decomposes over quotient fibers. When the weight is constant on classes, that fiber sum collapses to fiber cardinality times the value on a representative.
Class mass of a triangulation class $q$ is the sum of $\mu$ over the labeled fiber of $q$. By the module theorems it equals $|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep}, q)|)$, not bare $1/|\mathrm{Aut}|$ per class. The standing labeled $Z$ therefore pushes forward as $\sum_q \mathrm{classMass}(q)\cdot w(\mathrm{rep}, q)$ for class-constant $w$.
A kernel landmine (C1) is already detonated in the module: at bond number $B=2$, distinct labeled edges related by vertex swap give a fiber of cardinality $>1$, and $\mu < \mathrm{classMass}$ on that class. Scope is the labeled PathSum $Z$ only; the exact-shell $Z_{\mathrm{RS},uv}$ uses a separate quotient-sum convention.
proof idea
No proof body: this is a structure declaration. Each field is a bare Bool (some with inline doc-comments fixing the intended polarity: false for the invAut-class-sum claim and the quotient-first construction; red for continuum limit, substrate measure, and gap-1 bridge). The downstream value classPushforwardStatus assigns concrete booleans; those assignments are forced by rfl against the proved lemmas of the module, not by new reasoning inside this structure.
why it matters
Gives the machine-readable scoreboard for the class-pushforward half of Seven Gaps Crux-2. Downstream, classPushforwardStatus is the sole inhabitant shown: it sets the five closed flags true (generic fiber decomposition, class mass defined, $Z$ equals class pushforward, class mass is fiberCard times $\mu$, non-singleton fiber exhibited) and leaves the remaining red/false items unset in the snippet, matching the module header's honest tier list.
In the Recognition gravity stack this separates proved quotient bookkeeping from open continuum and substrate-measure work. It records the C1 detonation as status rather than prose: labeled $Z$ is not the inequivalent-class $1/|\mathrm{Aut}|$ sum. That distinction matters for any later bridge from discrete path-sum $Z$ toward continuum or gap-1 claims, which this wave explicitly does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.