module module moderate

`IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight`

Preflight lemmas for exact shell gauge counting in the Seven Gaps path-sum program. Establishes that gauge equivalence is an equivalence relation, that finite relabelings form a finite torsor over Aut, and that pair counts factor as orbit cardinality times |Aut|. Downstream measure work cites the identity that gauge-counting mass equals 1/|Aut|. Proofs are finite-set and group-action bookkeeping on BoundedComplex configurations.

claimOn the finite configuration class of bounded complexes, gauge relabeling is an equivalence relation. Writing $N_{\mathrm{pair}}$ for the number of (config, relabeling) pairs, $N_{\mathrm{orbit}}$ for the number of gauge orbits, and $|\mathrm{Aut}|$ for the automorphism order, one has $N_{\mathrm{pair}} = N_{\mathrm{orbit}} \cdot |\mathrm{Aut}|$ with both factors positive, so the uniform gauge-counting mass per orbit is $1/|\mathrm{Aut}|$.

background

Lane 2 of the Seven Gaps gravity stack builds a path-sum measure $Z_{RS}$ on a scoped configuration class BoundedComplex B. Upstream, PathSumMeasure proves that class is a Fintype via an explicit coding equivalence, so every counting argument is literally finite-set arithmetic rather than measure-theoretic existence.

Gauge structure enters as relabelings of incidence data. Two configurations are gauge-equivalent when one is the image of the other under a permitted relabeling. The module packages the orbit-stabilizer style counts: orbit cardinality, automorphism (relabeling) cardinality, and the pair count of configurations with chosen relabelings.

The local goal is not yet a unique physical measure. It is the exact combinatorial identity that any uniform average over gauge orbits assigns mass $1/|\mathrm{Aut}|$ to each orbit representative class, recorded cleanly before invariance no-go and substrate blocker arguments.

proof idea

The module is a short finite-group counting layer, not a single deep theorem. Reflexivity, symmetry, and transitivity of the gauge relation are the identity, inverse, and composition of relabelings. Finiteness of the relabeling type is inherited from the upstream Fintype structure on bounded complexes.

Orbit and pair cardinalities are defined by enumeration over that finite type. Positivity is immediate from inhabited data (identity relabeling). The key algebraic step is a torsor equivalence identifying relabelings with a free transitive Aut-action on fibers, which yields relabelingCount = |Aut| and the product formula pairCount = orbitCard * autCard. No analytic estimates appear.

why it matters in Recognition Science

MeasureSubstrateBlocker imports this module as the exact preflight for gauge-counting mass. Its doc-comment states the division of labor: ExactShellGaugePreflight proves the gauge-counting mass equals $1/|\mathrm{Aut}|$ and records uniform gauge density as a model premise, while MeasureInvarianceNoGo shows that relabeling invariance, positivity, and normalization alone do not select a path-sum measure.

In the Recognition gravity program this sits under the Seven Gaps effort to pin which combinatorial inputs are forced versus which remain model hypotheses when building $Z_{RS}$. The counting identity is the honest substrate for any later claim that shell or rung weights descend to gauge orbits without double-counting Aut copies. It does not by itself force Newton's constant, the $\phi$-ladder mass formula, or $D=3$; those live elsewhere in the forcing chain.

scope and limits

Does not construct a unique path-sum measure on configurations.
Does not prove relabeling invariance selects physical weights without extra premises.
Does not evaluate numerical Aut orders for concrete shells or galaxies.
Does not derive G, alpha, or mass-ladder rungs from gauge counting.
Does not remove the model status of the uniform gauge-density principle.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (34)

theorem equivalent_refl L96
theorem equivalent_symm L100
theorem equivalent_trans L105
instance instFiniteRelabel L112
def gaugeOrbitCard L122
def relabelingCount L126
def pairCount L133
theorem gaugeOrbitCard_pos L137
def torsorEquiv L147
theorem relabelingCount_eq_autCard L168
theorem pairCount_eq_orbitCard_mul_autCard L177
theorem pairCount_pos L188
theorem gaugeOrbitCard_congr L195
theorem autCard_congr L203
theorem pairCount_congr L210
theorem gaugeMassRep_congr L218
def orbitCardClass L226
theorem orbitCardClass_mk L229
def pairCountClass L233
theorem pairCountClass_mk L236
theorem pairCountClass_pos L239
def gaugeOrbitMass L247
theorem gaugeOrbitMass_eq_mu L254
theorem gaugeOrbitMass_mul_pairCount L268
theorem gaugeCountingMass_unique L281
instance instFintypeTriangulationClass L294
theorem labeledZ_eq_orbitWeighted_classSum L303
structure GaugePreflightStatus L352
def gaugePreflightStatus L361
theorem status_gauge_torsor L367
theorem status_measure_derived L369
theorem status_uniqueness L371
theorem status_counting_principle_open L375
theorem gaugePreflight_grounded L381