R04
plain-language theorem explainer
Proposition asserting that for every triangulation bound B ≥ 2, the constant (uniform) mass on combinatorial classes fails the gauge-counting principle. The Gap-2 necessary-reasons census cites it to show GCP is strictly stronger than mere class invariance. It is a bare Prop; discharge is by the sibling theorem that the two-point class forces mass 1/2.
Claim. For every natural number $B \ge 2$, the constant class mass $\nu \equiv 1$ on combinatorially distinct triangulations of bound $B$ does not satisfy the gauge-counting principle: class mass times gauge-witness volume need not equal labeled orbit size.
background
Gap-2 in the gravity measure program asks which extra principle pins the physical class mass on the quotient of labeled triangulations by relabeling. A triangulation class is that quotient; the gauge-counting principle (GCP) demands that for every class $c$, mass($c$) times the gauge-witness volume equals the labeled orbit cardinality.
Uniform class mass is the constant function $1$ on classes. Module framing treats it as the live decoy admitted by weaker invariance axioms alone: any principle that only forces class-level invariance still allows this flat assignment. Upstream, the counting-defined orbit mass is known to satisfy GCP, so the contrast is sharp.
This module runs a necessary-reasons census: every candidate fact that would make GCP unavoidable is scored THEOREM, OPEN, MODEL, or REFUTED. The present declaration is the Prop slot for the uniform-decoy failure.
proof idea
Definitional, not a proof. The body is the universal statement that for all $B \ge 2$, GCP fails at uniform class mass. No tactics or lemmas are applied here; the mathematical work lives in the sibling that exhibits a concrete class (the two-point class, required mass $1/2$) where constant mass $1$ breaks the identity mass × pair-count = orbit card. Downstream R04_reason is the one-line wrapper that intro's $B$ and applies that failure theorem.
why it matters
In the Gap-2 gauge-counting census this is reason R04: "uniform class mass fails GCP," scored THEOREM in the reason table. It pairs with R03 (counting mass satisfies GCP) and R02 (GCP iff the mass equals gauge-orbit mass) to show the extra principle is discriminating, not a restatement of class invariance.
Parents are R04_reason (inhabits the Prop), the reason table entry, and the broader necessary-reasons process that filters which richer RecognitionLedger or posting-layer structure could force GCP. Several enrichment, gluing, and label-indifference routes are already REFUTED as GCP derivations; this entry keeps the floor plan honest by killing the flat decoy. It does not itself select the physical measure; it only rules out one underdetermined alternative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.