does
plain-language theorem explainer
The labeled path-sum partition function Z is not the Burnside-style sum over inequivalent triangulation classes with weight 1/|Aut|. Class pushforward mass equals |fiber|·(1/|Aut|), and fibers need not be singletons. Gravity path-sum bookkeeping cites this as the Crux-2 fork verdict. Separation is the kernel inequality μ < classMass on the B=2 edge class.
Claim. The labeled path sum $Z$ (sum of $\mu(K)\,w(K)$ over labeled bounded complexes) does not equal the sum over inequivalent classes with weights $1/|\mathrm{Aut}|$. The class-pushforward weight is $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep}\,q)|)$, and already at bond bound $B=2$ one has $\mu(K)<\mathrm{classMass}([K])$ for the one-edge class, so the two schemes differ as a kernel fact.
background
Module Crux-2 (Seven Gaps, path-sum pillar) locks the protocol QUOTIENT_BOOKKEEPING: finite sums over labeled complexes push forward to the quotient by relabeling. For a setoid on a fintype, any additive sum decomposes fiberwise; when the summand is class-constant it collapses to fiber cardinality times the value on a representative.
Path-sum measure assigns each labeled complex $K$ the symmetry weight $\mu(K)=1/|\mathrm{Aut}(K)|$. The class mass of a quotient point $q$ is the sum of $\mu$ over the labeled fiber, equivalently $|\mathrm{fiber}(q)|\cdot(1/|\mathrm{Aut}(\mathrm{rep},q)|)$ by the fiber-card identity. $Z$ is the labeled sum; the class pushforward identity rewrites it as $\sum_q \mathrm{classMass}(q),w(\mathrm{rep},q)$ whenever $w$ is constant on classes.
Upstream, exists_nonSingleton_fiber exhibits two distinct $B=2$ one-edge complexes related by a vertex-swap relabeling, so some fiber has cardinality $>1$. The numeric witness mu_lt_classMass_edgeClass then proves $\mu(\mathrm{edgeAB})<\mathrm{classMass}([\mathrm{edgeAB}])$.
proof idea
No separate algebraic expansion is needed beyond the fork lemmas. Non-singleton fibers at $B=2$ give $|\mathrm{fiber}|>1$ on the one-edge class. Combined with positivity of $\mu$ and congruence of $\mu$ on equivalent complexes, the identity $\mathrm{classMass}=|\mathrm{fiber}|\cdot\mu(\mathrm{rep})$ forces $\mu(\mathrm{rep})<\mathrm{classMass}$. Therefore any class decomposition of the standing labeled $Z$ carries $|\mathrm{fiber}|/|\mathrm{Aut}|$ per class and cannot coincide with the pure $1/|\mathrm{Aut}|$ inequivalent-class sum. The declaration packages that negative identification as the kernel fact.
why it matters
In the Seven Gaps path-sum story this is the C1 landmine detonation: it blocks the silent identification of labeled $Z$ with a Burnside $1/|\mathrm{Aut}|$ class sum. Downstream class-pushforward equalities ($Z$ and the RS variant equal the classMass-weighted quotient sum) inherit the correct weight; using $1/|\mathrm{Aut}|$ alone would be a different convention.
Scope is deliberately narrow: only the labeled PathSum.Z of the path-sum measure. The exact-shell $Z_{RS}$ objects use a quotient-sum convention by their own headers; the two conventions are not a contradiction. Within Recognition gravity this keeps quotient bookkeeping honest before continuum or curvature limits are taken. It does not itself force $D=3$, the eight-tick octave, or the $\varphi$-ladder mass formula; those live on other chain steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.