classPushforwardStatus_flags
plain-language theorem explainer
Status ledger for the class-pushforward bookkeeping of the labeled path-sum partition function Z under the Seven Gaps Crux-2 protocol. It records five items as proved (generic fiber decomposition, class mass, Z equals the class pushforward, class mass equals fiber cardinality times mu, and a non-singleton fiber) and five as still open. Auditors of quotient bookkeeping cite it to see the honest flag set. The proof is ten reflexivity checks against the status structure.
Claim. The class-pushforward status record asserts that generic fiber decomposition, the definition of class mass, the identity $Z=\sum_q \mathrm{classMass}(q)\,w(\mathrm{rep}\,q)$ for class-constant weights, the relation $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot\mu$, and exhibition of a non-singleton fiber are all marked true, while the inverse-Aut class-sum form of $Z$, a quotient-first object, the continuum limit of $Z_{\mathrm{RS}}$, derivation of the substrate measure, and the gap-1 bridge remain marked false.
background
Module setting is Seven Gaps Crux-2 (pillar 2, path-sum): class pushforward of the labeled partition function $Z$ under the locked QUOTIENT_BOOKKEEPING protocol. For a finite type with a setoid, any additive monoid-valued function decomposes as a sum over quotient fibers; when the function is constant on classes the fiber sum collapses to fiber cardinality times the value on a representative.
Class mass of a triangulation class $q$ is the sum of the labeled measure $\mu$ over the fiber of $q$. When the weight $w$ is constant on classes, $Z$ equals the pushforward $\sum_q \mathrm{classMass}(q)\cdot w(\mathrm{rep},q)$. By the fiber identity, class mass is $|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$, not bare $1/|\mathrm{Aut}|$ per class.
Upstream, the status structure hard-codes the five true flags and five false flags that this theorem re-exports. A kernel fact at bond number $B=2$ exhibits a non-singleton fiber (two distinct labeled edges related by vertex swap), so the labeled $Z$ already differs numerically from an inequivalent-class sum weighted only by $1/|\mathrm{Aut}|$.
proof idea
Pure term-mode proof: a 10-tuple of rfl. Each conjunct equates one field of the status structure to the Boolean literal written in that structure's definition, so reflexivity discharges every equality. No lemmas are applied beyond the definitional unfolding of the status record.
why it matters
Honest status tagging for Crux-2 quotient bookkeeping in the gravity Seven Gaps program. It freezes, as a proved theorem rather than prose, which pieces of the class-pushforward story are closed (generic fiber sum, class mass, $Z$ as class pushforward, mass equals fiber card times $\mu$, non-singleton fiber at $B=2$) and which remain open (inverse-Aut class-sum convention for $Z$, quotient-first construction, continuum limit of $Z_{\mathrm{RS}}$, substrate measure derivation, gap-1 bridge).
No downstream consumers are wired yet; the declaration is the module's terminal status certificate. The fork verdict it records matters for Recognition gravity: the labeled path-sum $Z$ carries $|\mathrm{fiber}|\cdot(1/|\mathrm{Aut}|)$ per class and is not interchangeable with a pure $1/|\mathrm{Aut}|$ class sum. Scope is deliberately narrow: the detonation applies only to the labeled PathSum $Z$, not to the exact-shell $Z_{\mathrm{RS}}$ quotient convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.