module module moderate

`IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV`

Defines the exact-shell gauge UV layer for Seven Gaps gravity: complexity of a bounded complex (max of vertex, edge, tetrahedron counts) as the shell coordinate, plus ExactComplex and ExactRelabel with congruence and equivalence laws. Downstream regulator-removal no-go cites the Gaussian-regulated quotient path sum built here. Mostly definitional scaffolding with elementary count equalities under relabeling.

claimFor a bounded incidence complex $C$, the shell coordinate (complexity) is $\mathrm{cx}(C) := \max\{|V(C)|, |E(C)|, |T(C)|\}$. An exact complex is a bounded complex equipped with this shell data; exact relabelings are incidence-preserving bijections that preserve $n_V$, $n_E$, $n_T$ (hence complexity), forming an equivalence relation with the usual reflexivity, symmetry, and transitivity.

background

Seven Gaps Lane 2 builds a path-sum measure $Z_{RS}$ over a configuration class of bounded incidence data. Upstream, PathSumMeasure introduces the garbage-inclusive superclass BoundedComplex B and proves it is a Fintype via an explicit coding equivalence. SimplicialClass carves out the simplicial subclass of that path-sum configuration class (full theory phase 0b), with finite combinatorial checks only on an explicit one-tetrahedron witness.

This module sits on those two imports and names the UV shell bookkeeping used for gauge-fixed exact complexes: vertex, edge, and tetrahedron counts, and their maximum as the shell coordinate. Exact relabelings are the natural isomorphisms of that discrete data; the module records that they preserve the three counts and therefore complexity.

proof idea

Definition-heavy module. Complexity is the pointwise max of the three finite counts. Relabel lemmas are direct transport of $n_V$, $n_E$, $n_T$ along the vertex/edge equivalences of an exact relabeling, then complexity_congr follows because max is congruence-invariant. ExactRelabel is packaged as a reflexive-symmetric-transitive relation (with explicit trans_vEquiv / trans_eEquiv composition of the underlying bijections). No deep analytic argument lives here; the analytic content is deferred to the regulated path sum that consumes these shells.

why it matters in Recognition Science

Feeds RegulatorRemovalNoGo, which proves that the Gaussian-regulated quotient path sum $Z_{RS,\mathrm{uv}}$ constructed from this exact-shell gauge UV layer has no $\rho \to 0^+$ limit at zero phase (kernel no-go). That no-go is the named open obstruction at vanishing phase for removing the UV regulator inside the Seven Gaps gravity program.

In the broader Recognition gravity stack, shell coordinates organize the discrete configuration sum before continuum or continuum-limit claims. Exactness and relabel invariance keep the measure well-defined on isomorphism classes of bounded complexes rather than on raw labeled incidence data, which is the minimal hygiene needed before any path-sum or regulator analysis.

scope and limits

Does not construct or evaluate the path sum $Z_{RS}$ or $Z_{RS,\mathrm{uv}}$ itself.
Does not prove existence or non-existence of any $\rho \to 0$ regulator limit.
Does not restrict to simplicial complexes only; that lives upstream in SimplicialClass.
Does not fix physical units, couplings, or Recognition constants ($c$, $\hbar$, $G$, $\phi$).
Does not claim continuum gravity or Einstein equations from the shell coordinate.

used by (1)

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

IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import
IndisputableMonolith.Gravity.SevenGaps.SimplicialClass module_import

declarations in this module (75)

def complexity L79
theorem relabel_nV_eq L84
theorem relabel_nE_eq L91
theorem relabel_nT_eq L98
theorem complexity_congr L106
structure ExactComplex L118
structure ExactRelabel L126
def refl L140
def symm L148
def trans L163
theorem trans_vEquiv L174
theorem trans_eEquiv L177
theorem trans_tEquiv L180
theorem symm_vEquiv L183
theorem symm_eEquiv L185
theorem symm_tEquiv L187
def toEquivTriple L192
theorem toEquivTriple_injective L198
theorem ext L209
def GlobalEquivalent L222
def exactSetoid L227
def exactCodeEquiv L237
instance instFintypeExactComplex L246
theorem exactComplex_card_eq L251
theorem exactComplex_card_le L260
abbrev ShellSig L291
abbrev sigV L296
abbrev sigE L298
abbrev sigT L300
theorem shellSig_card_le L303
abbrev ExactPathClass L319
instance instFiniteExactQuotient L322
instance instFintypeExactPathClass L327
def exactComplexity L334
theorem shell_index_unique L342
def toExact L351
theorem toExact_relax L359
theorem toExact_complexity L363
theorem exactPathClass_card_le L374
def isolatedVertices L409
def isolatedSig L414
def isolatedClass L421
instance instNonemptyExactPathClass L424
theorem exactPathClass_unbounded_support L430
abbrev ExactAut L438
instance instFiniteExactAut L445
theorem exactAutCard_pos L451
def exactMu L457
theorem exactMu_pos L461
theorem exactMu_le_one L468
theorem exactMu_congr L502
def classMuOn L509
def classMu L514
theorem classMu_pos L518
theorem classMu_le_one L523
def liftedPhase L531
def zRSUVShell L545
theorem norm_zRSUVShell_le L553
theorem norm_zRSUVShell_le_entropy L578
theorem log_le_linear L596
theorem exists_gaussian_domination L608
theorem pow_eq_exp_log L663
theorem summable_zRSUVShell L674
def Z_RS_uv L718
theorem zRSUVCutoff_tendsto L724
def zeroPhase L734
def shellMass L737
theorem shellMass_pos L742
theorem zRSUVShell_zeroPhase_eq L747
theorem zRSUVShell_zeroPhase_re_pos L759
theorem Z_RS_uv_zeroPhase_re_pos L768
def HasZRSRegulatorRemoval L796
structure ExactShellGaugeUVStatus L811
def exactShellGaugeUVStatus L831
theorem exactShellGaugeUVStatus_grounded L843