Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker

show as:
view Lean formalization →

Isolates the exact extra principle beyond measure invariance that the gauge-counting derivation of the path-sum weight needs: class mass times gauge-witness volume equals labeled orbit size. Supplies the substrate-measure blocker certificate contrasting gauge-orbit mass with uniform class mass. The full-theory ledger imports it as a Lane D status record. Argument is definitional packaging plus iff lemmas and an explicit non-equality witness.

claimThe gauge-counting principle states that class mass times gauge-witness volume equals labeled orbit size. The substrate measure blocker records that relabeling invariance alone does not force $\mu=1/|\mathrm{Aut}|$, and that uniform class mass is not the gauge-counting measure on representatives.

background

In the Seven Gaps gravity campaign, the scoped path-sum measure is the discrete weight $\mu$ on combinatorial classes. The standard convention is the symmetry factor $\mu K = 1/|\mathrm{Aut}, K|$. ExactShellGaugePreflight derives that weight from pure gauge counting, using a gauge mass that never mentions $\mu$ or $\mathrm{Aut}$ by name.

MeasureInvarianceNoGo is the matching kill: relabeling invariance plus positivity and normalization do not single out $\mu = 1/|\mathrm{Aut}|$. Explicit alternative measures survive those axioms. An extra structural principle is therefore required.

This module names that principle. Gauge-counting equates class mass times gauge-witness volume with labeled orbit size. Uniform class mass is exhibited as a concrete counter-model to the claim that any invariant mass is already gauge-counting.

proof idea

Definitional core: introduce the gauge-counting principle as a Prop on class masses, and the gauge-orbit mass that satisfies it by construction. Iff lemmas equate the principle with (i) equality to gauge-orbit mass and (ii) the representative formula for $\mu$. Uniform class mass is defined separately; a short non-equality proof shows it fails the principle. The blocker certificate packages the no-go import with that witness into a single status object for the ledger.

why it matters in Recognition Science

Closes the logical gap between the invariance no-go and the constructive gauge-counting derivation. Without an explicit extra principle, the $1/|\mathrm{Aut}|$ weight would remain a postulate rather than a derived object. FullTheoryLedger imports the module as part of the Phase 0c benchmark record: one boolean flag per pillar, flipped only when the target is kernel-checked and critic-passed. The blocker certificate is the machine-checked status token for the measure-substrate lane, preventing silent reintroduction of "invariance alone determines $\mu$".

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)