uniformClassMass
plain-language theorem explainer
Assigns mass one to every triangulation class on the path-sum quotient. It is the explicit decoy still allowed by relabeling invariance, positivity, and normalization. Downstream blocker theorems cite it to show that normalized gauge counting is strictly stronger: on the two-point class the required mass is one-half, so this constant assignment fails. The definition is the constant function.
Claim. For each bound $B\in\mathbb{N}$, the uniform class mass is the function $\mu_{\mathrm{unif}}:\{\text{triangulation classes of bound }B\}\to\mathbb{R}$ given by $\mu_{\mathrm{unif}}(K)=1$ for every class $K$.
background
The module sits in the gravity seven-gaps ledger for path-sum measures. MeasureInvarianceNoGo already shows that relabeling invariance, positivity, and normalization do not pick a unique measure on triangulation classes. Exact shell preflight records that the intended gauge-counting mass on a class is $1/|\mathrm{Aut}|$, and treats normalized gauge counting as a model premise rather than a consequence of those weaker axioms.
A class mass satisfies normalized gauge counting when its mass times the number of (labeled copy, relabeling witness) pairs recovers the number of labeled copies. Equivalently, every class must carry mass $1/|\mathrm{Aut}|$. The uniform assignment on quotient classes is the natural decoy still compatible with pure class invariance: it spreads mass evenly across classes, ignoring automorphism size.
The two-point class is the discriminating test case. There $|\mathrm{Aut}|=2$, so gauge counting demands mass $1/2$, while the uniform decoy still assigns $1$.
proof idea
Definitional: the body is the constant function sending every triangulation class to the real number $1$. No lemmas are applied; there is no proof obligation beyond the type TriangulationClass B → ℝ.
why it matters
This decoy is the concrete witness that the remaining substrate gap is real. The sibling theorem uniformClassMass_not_gaugeCounting uses it to prove failure of normalized gauge counting on every $B\ge 2$, via the two-point class where the required mass is $1/2$. That fact is packaged into substrate_measure_blocker_certificate and lifted to the full-theory ledger as gap2_measure_selection_blocker_certified.
In ledger language, Pillar 2's measure half is certified open at exactly one premise: a derivation of normalized gauge counting (equivalently $1/|\mathrm{Aut}|$) from richer structure, not from invariance or from renaming uniform quotient counting. The continuum-limit half of the same gap stays separately open. The definition itself flips no ledger flag; it only supplies the decoy the blocker theorems refute.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.