gap2_measure_selection_blocker_certified
plain-language theorem explainer
For every triangulation bound B ≥ 2, normalized gauge-orbit mass satisfies the gauge-counting principle, that principle is equivalent to assigning each class the reciprocal automorphism weight 1/|Aut K|, and the uniform class-mass decoy fails it. Gravity and path-sum workers cite this as the certified measure half of the Pillar-2 continuum-and-measure gap. The proof is a one-line term wrapper of the substrate measure-blocker certificate.
Claim. For every integer $B \ge 2$: (i) the exact-shell gauge-orbit mass on triangulation classes of bound $B$ obeys the gauge-counting principle; (ii) a real weight $\nu$ on those classes obeys the principle if and only if $\nu([K]) = \mu(K)$ for every bounded complex $K$ of bound $B$, where $\mu$ is the reciprocal-automorphism weight; (iii) the uniform class-mass weight does not obey the principle.
background
This module is the full-theory ledger for the quantum-gravity campaign: three pillars (classical recovery, a well-defined quantum amplitude, and at least one discriminating prediction), with boolean flags that flip only under kernel-checked theorems. Pillar 2 demands a substrate-to-geometry bridge plus a path-sum measure with a proved continuum/convergence limit.
The measure half of that obligation is isolated here. Path-sum weights live on triangulation classes (quotients of bounded complexes by relabeling). The gauge-counting principle requires the weight to be the normalized orbit mass, equivalently $\mu(K) = 1/|\mathrm{Aut}, K|$. A uniform decoy that spreads mass evenly across classes is the natural false alternative.
The continuum-limit half of the same gap (late-block smallness of shell amplitudes and capped $Z_q$ compatibility) is certified separately; this declaration treats only measure selection.
proof idea
One-line term wrapper: the proof is exactly the application of MeasureSubstrateBlocker.substrate_measure_blocker_certificate, which already packages the three conjuncts (orbit mass satisfies the principle; the principle is equivalent to $\nu([K])=\mu(K)$; uniform class mass fails). No local tactic work; the ledger merely re-exports the certificate under the gap-2 name for the full-theory benchmark.
why it matters
Inside the full-theory ledger this is the certified measure blocker for Pillar 2: the measure half of the continuum-and-measure gap is open at one exact premise. Normalized gauge counting is forced as the unique principle-satisfying weight, and the quotient-uniform decoy is ruled out on a concrete two-point class. A closing theorem must therefore derive $1/|\mathrm{Aut}, K|$ from richer substrate structure rather than postulate it.
The continuum-limit half remains separately open (complexity-cutoff statements on late shell blocks and capped $Z_q$ compatibility, not mesh refinement). Downstream, the master claim full_theory_not_yet_closed stays provable until every pillar flag flips; this certificate keeps the measure flag honest. No used-by edges yet: the declaration is a ledger status record, not an intermediate lemma in a longer chain.
Framework context: path-sum measure selection sits under the quantum-amplitude pillar that must eventually connect substrate recognition structure (eight-tick octave, $D=3$ forcing) to a continuum geometric amplitude.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.