mu_lt_classMass_edgeClass
plain-language theorem explainer
At the B=2 edge class, the labeled measure of one representative is strictly below the pushforward class mass: μ(edgeAB) < classMass([edgeAB]). Anyone separating the labeled path-sum Z from an inequivalent-class sum weighted by 1/|Aut| cites this numeric fork. The proof rewrites class mass as fiber cardinality times μ, then multiplies the positive measure by a fiber size strictly larger than one.
Claim. Let $\mathrm{edge}_{AB}$ be the labeled two-vertex edge complex at bond count $B=2$. Write $\mu$ for its labeled Aut-weight and $\mathrm{classMass}(q)$ for the sum of $\mu$ over the relabeling fiber of class $q$. Then $\mu(\mathrm{edge}_{AB}) < \mathrm{classMass}([\mathrm{edge}_{AB}])$.
background
Module Crux-2 (Seven Gaps, path-sum pillar) studies the class pushforward of the labeled path-sum $Z$. Complexes at fixed bond count $B$ are quotiented by vertex relabeling; each class $q$ has a fiber of labeled representatives and a class mass equal to the sum of the labeled measure $\mu$ over that fiber.
By the sibling identity, class mass factors as fiber cardinality times $\mu$ of any representative: $\mathrm{classMass}(q)=|\mathrm{fiber}(q)|\cdot\mu(\mathrm{rep},q)$. Here $\mu$ is the labeled Aut-weight $1/|\mathrm{Aut}|$, not a bare symmetry factor per class. The module already exhibits a non-singleton fiber at $B=2$: $\mathrm{edge}{AB}$ (edge $(0,1)$) and $\mathrm{edge}{BA}$ (edge $(1,0)$) are distinct labeled complexes related by an explicit vertex swap, so the fiber of $[\mathrm{edge}_{AB}]$ has cardinality strictly greater than one.
The standing $Z$ of PathSumMeasure is the labeled sum. When a weight is constant on classes, $Z$ decomposes as a sum of classMass$(q)$ times the weight on a representative. That decomposition is what this inequality probes numerically.
proof idea
First align the representative: $\mu$ of Quotient.out of the class equals $\mu(\mathrm{edge}_{AB})$ by congruence of $\mu$ under the relabeling equivalence (from Quotient.out_eq). Rewrite class mass via the fiber-card identity, substituting that representative equality.
Cast the already-proved fact that the edge-class fiber has cardinality $>1$ to a real inequality $1<|\mathrm{fiber}|$. Then a one-line calc: $\mu=1\cdot\mu$, and multiply on the right by the positive measure $\mu(\mathrm{edge}_{AB})$ to get $1\cdot\mu<|\mathrm{fiber}|\cdot\mu$. Positivity of $\mu$ supplies the strictness.
why it matters
This is the T3 fork verdict of the class-pushforward wave: a kernel-level numeric witness that classMass is not $1/|\mathrm{Aut}|$ per class. The labeled path-sum $Z$ therefore cannot be rewritten as an inequivalent-class sum with bare Aut weights; the two conventions already separate at $B=2$.
Downstream, the status ledger ClassPushforwardStatus records the wave's proved flags (fiber decomposition, classMass definition, $Z$ pushforward identity, fiber-card factorization, non-singleton fiber). A sibling theorem states explicitly that $Z$ does not equate to the inequivalent-class $1/|\mathrm{Aut}|$ sum, citing this inequality and the non-singleton fiber exhibition as the separation.
In the Seven Gaps gravity bookkeeping this closes the labeled-versus-quotient ambiguity for PathSum.Z only. It does not touch the exact-shell $Z_{RS}$ convention, which uses quotient-sum weights by design. No forcing-chain landmark (T5–T8, RCL, $\phi$) is invoked; the result is pure finite quotient measure arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.