uniformClassMass_not_gaugeCounting
plain-language theorem explainer
The quotient-uniform class mass on triangulation classes fails the normalized gauge-counting principle whenever the bond count is at least 2. Anyone arguing that path-sum measure is fixed by invariance alone would cite this: the uniform decoy is ruled out on the two-point class, where gauge counting demands mass 1/2. The proof reduces the principle to a representative measure identity and obtains a numerical contradiction via the two-point complex.
Claim. For every integer $B \ge 2$, the quotient-uniform class mass $\nu_{\mathrm{unif}} : \mathrm{TriangulationClass}(B) \to \mathbb{R}$ does not satisfy the gauge-counting principle: it is not the case that $\nu_{\mathrm{unif}}(c) \cdot |\mathrm{pairCount}(c)| = |\mathrm{orbit}(c)|$ for every class $c$.
background
In the path-sum measure program, class masses assign real weights to triangulation classes at bond count $B$. Relabeling invariance, positivity, and normalization alone do not pick a unique measure (MeasureInvarianceNoGo). The extra selection rule is the gauge-counting principle: class mass times the volume of (labeled copy, relabeling witness) pairs equals the labeled orbit size. Equivalently, every class must carry mass $1/|\mathrm{Aut}|$.
The counting-defined gauge-orbit mass satisfies that principle. The quotient-uniform decoy instead spreads mass evenly across classes in the quotient, ignoring automorphism size. The module isolates this decoy and shows it is not a silent restatement of class invariance.
The decisive test object is the two-point complex: on that class the gauge-counting mass is $1/2$, while the uniform assignment disagrees after the representative-measure rewrite.
proof idea
Assume for contradiction that the uniform class mass obeys the gauge-counting principle. The equivalence gaugeCountingPrinciple_iff_mu_on_representatives converts that assumption into an identity between the uniform mass and the representative measure $\mu$ on every bounded complex, specialized here to the two-point complex. Unfolding the uniform mass and rewriting with mu_twoPointComplex produces a concrete numerical equation. norm_num discharges the contradiction (the two sides are unequal rationals, with gauge counting requiring $1/2$).
why it matters
This is the discriminating half of the substrate blocker: gauge counting is not empty invariance language, because the natural uniform decoy fails it. Downstream, R04_uniform_fails and the history re-export decoy_uniformClassMass_not_gaugeCounting cite it verbatim. The package theorem substrate_measure_blocker_certificate conjoins the positive fact (gauge-orbit mass satisfies the principle and equals $1/|\mathrm{Aut}|$) with this negative fact, concluding that the remaining task is a ledger derivation of gauge counting, not more measure-invariance axioms.
In the Seven Gaps gravity stack this closes a no-go fork: path-sum measure cannot be finished by renaming uniform quotient counting. It forces the richer ledger structure that supplies normalized gauge counting. No FullTheoryLedger flag is flipped here; the certificate only pins the blocker.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.