substrate_measure_blocker_certificate
plain-language theorem explainer
For any bound B ≥ 2, normalized gauge counting holds for the orbit-over-pair class mass, is equivalent to assigning every class the representative mass μ, and fails for the quotient-uniform decoy. Gravity gap-2 ledger work cites this as the certified measure-selection blocker. The proof is a three-component term packing three already-proved sibling lemmas.
Claim. For every integer $B \ge 2$, the class mass $\nu_{\mathrm{orbit}}(c) = |\mathrm{orbit}(c)|/|\mathrm{pairs}(c)|$ satisfies the gauge-counting principle $\nu(c)\cdot|\mathrm{pairs}(c)| = |\mathrm{orbit}(c)|$; a class mass $\nu$ satisfies that principle if and only if $\nu([K]) = \mu(K)$ for every bounded complex $K$; and the uniform class mass on the triangulation quotient fails the principle.
background
The SevenGaps gravity stack isolates continuum and measure gaps in the path-sum substrate. MeasureInvarianceNoGo already shows that relabeling invariance, positivity, and normalization do not pick a unique path-sum measure. Exact-shell preflight defines the gauge-orbit mass of a triangulation class as labeled orbit cardinality over pair-count (gauge-witness volume), and records that this equals $1/|\mathrm{Aut}|$ once orbit-stabilizer is applied.
This module names the missing premise exactly. The gauge-counting principle asserts that class mass times pair-count equals orbit cardinality. Equivalently, every class receives the representative mass $\mu$ pulled back along the relabeling quotient. The uniform mass on quotient classes is the natural decoy that still looks invariant but fails the counting identity on a concrete two-point class when $B \ge 2$.
Local setting: the remaining substrate task is not more invariance; it is a ledger derivation of normalized gauge counting from richer structure.
proof idea
Term-mode triple. First component is the sibling lemma that the counting-defined orbit mass satisfies the gauge-counting principle by direct cancellation of the pair-count denominator. Second component is the equivalence lemma: a class mass obeys the principle iff it agrees with $\mu$ on every relabeling class representative. Third component is the decoy lemma uniformClassMass_not_gaugeCounting, which needs $B \ge 2$ to exhibit a two-point class where uniform quotient mass violates the pair-count identity. No new algebra is done here; the certificate only packages the three facts.
why it matters
This is the certified measure half of gravity gap 2. Downstream, gap2_measure_selection_blocker_certified in FullTheoryLedger quotes it as the pillar-2 measure blocker: normalized gauge counting is equivalent to $1/|\mathrm{Aut}|$, the uniform decoy fails on a concrete class, and a closing theorem must derive the principle from richer ledger structure (continuum half stays separately open). The residual DAG uses it to inhabit typedResidual_measure_gaugeCounting_blocker, and the hostile-probe module exposes blocker_certificate_available from the same package.
In the Recognition stack this pins what invariance cannot finish: path-sum measure selection is blocked at one exact premise, not at a vague continuum slogan. It flips no FullTheoryLedger flag; it certifies the open residual so later ledger work knows the precise obligation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.