IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV
Defines exact-shell complexes, shell complexity as the max of vertex/edge/tetrahedron counts, and relabeling gauge equivalence for the UV-regulated Recognition path sum. Gravity and Gap-2 continuum authors cite it when fixing shells before continuum or regulator limits. The module is mostly definitional, with congruence lemmas showing complexity is invariant under exact relabeling.
claimOn bounded incidence configurations, an exact complex carries finite vertex, edge, and tetrahedron counts $n_V,n_E,n_T$. Its shell complexity is $C=\max(n_V,n_E,n_T)$, the shell coordinate. Exact relabeling is an equivalence of exact complexes preserving incidence up to bijections of the three sorts; complexity is constant on equivalence classes and supplies the gauge-fixed UV shell for the regulated path sum $Z_{RS}^{uv}$.
background
Seven Gaps Lane 2 builds a path-sum measure $Z_{RS}$ on a scoped configuration class. Upstream, BoundedComplex B is the garbage-inclusive superclass of bounded incidence data (proved a Fintype via an explicit code equivalence). The simplicial subclass cuts that superclass down to configurations whose incidence is genuinely simplicial, with a one-tetrahedron witness checked by finite combinatorial decide.
This module sits on that stack and isolates the exact-shell layer used for UV gauge fixing. Complexity of a bounded complex is defined as the largest of its vertex, edge, and tetrahedron counts; the doc-comment states that this integer is the shell coordinate. Exact complexes and exact relabelings package the residual gauge freedom (vertex/edge/tetrahedron bijections compatible with incidence) so that path-sum weights can be summed shell-by-shell without double-counting labelings.
Notation throughout is combinatorial: $n_V,n_E,n_T$ for the three counts, complexity for their max, and a small equivalence-relation API (refl/symm/trans plus transport of the count equalities) for relabeling.
proof idea
Definition-and-congruence module rather than a deep existence proof. Complexity is introduced as the max of the three finite counts. Separate lemmas record that exact relabeling preserves $n_V$, $n_E$, and $n_T$ individually, then a congruence lemma lifts those equalities to equality of complexity. The relabeling relation is equipped with the standard equivalence-relation package (reflexivity, symmetry, transitivity) and transport lemmas for the underlying vertex and edge equivalences. No analytic estimates or continuum limits are proved here; those are deferred to importers.
why it matters in Recognition Science
Exact-shell gauge UV is the named carrier of the Gaussian-regulated quotient path sum $Z_{RS}^{uv}$. Downstream, RegulatorRemovalNoGo cites it to prove a kernel no-go: that regulated sum has no $\rho\to 0^+$ limit at zero phase. Gap-2 continuum residual DAG and posting-history continuum residual modules import it when banking ordered residuals for Pillar-2 measure and continuum-limit recovery. The Aut-fiber parity blocker also depends on exact shells when partitioning equal-shellAutCard classes inside one shell for the antipodal matching route.
In the broader Recognition gravity program this is the combinatorial UV bookkeeping layer between the proved path-sum measure on bounded complexes and the open continuum/regulator questions. It does not close those questions; it fixes the shell coordinate and gauge so later no-gos and residual DAGs can be stated cleanly.
scope and limits
- Does not construct the continuum limit of $Z_{RS}^{uv}$ or prove regulator removal.
- Does not assert that every BoundedComplex is exact or simplicial.
- Does not evaluate numerical path-sum weights or mass-ladder constants.
- Does not prove Aut-fiber parity or antipodal matching; only supplies shell structure those APIs import.
- Does not introduce new physical axioms beyond the upstream path-sum configuration class.
used by (4)
depends on (2)
declarations in this module (75)
-
def
complexity -
theorem
relabel_nV_eq -
theorem
relabel_nE_eq -
theorem
relabel_nT_eq -
theorem
complexity_congr -
structure
ExactComplex -
structure
ExactRelabel -
def
refl -
def
symm -
def
trans -
theorem
trans_vEquiv -
theorem
trans_eEquiv -
theorem
trans_tEquiv -
theorem
symm_vEquiv -
theorem
symm_eEquiv -
theorem
symm_tEquiv -
def
toEquivTriple -
theorem
toEquivTriple_injective -
theorem
ext -
def
GlobalEquivalent -
def
exactSetoid -
def
exactCodeEquiv -
instance
instFintypeExactComplex -
theorem
exactComplex_card_eq -
theorem
exactComplex_card_le -
abbrev
ShellSig -
abbrev
sigV -
abbrev
sigE -
abbrev
sigT -
theorem
shellSig_card_le -
abbrev
ExactPathClass -
instance
instFiniteExactQuotient -
instance
instFintypeExactPathClass -
def
exactComplexity -
theorem
shell_index_unique -
def
toExact -
theorem
toExact_relax -
theorem
toExact_complexity -
theorem
exactPathClass_card_le -
def
isolatedVertices -
def
isolatedSig -
def
isolatedClass -
instance
instNonemptyExactPathClass -
theorem
exactPathClass_unbounded_support -
abbrev
ExactAut -
instance
instFiniteExactAut -
theorem
exactAutCard_pos -
def
exactMu -
theorem
exactMu_pos -
theorem
exactMu_le_one -
theorem
exactMu_congr -
def
classMuOn -
def
classMu -
theorem
classMu_pos -
theorem
classMu_le_one -
def
liftedPhase -
def
zRSUVShell -
theorem
norm_zRSUVShell_le -
theorem
norm_zRSUVShell_le_entropy -
theorem
log_le_linear -
theorem
exists_gaussian_domination -
theorem
pow_eq_exp_log -
theorem
summable_zRSUVShell -
def
Z_RS_uv -
theorem
zRSUVCutoff_tendsto -
def
zeroPhase -
def
shellMass -
theorem
shellMass_pos -
theorem
zRSUVShell_zeroPhase_eq -
theorem
zRSUVShell_zeroPhase_re_pos -
theorem
Z_RS_uv_zeroPhase_re_pos -
def
HasZRSRegulatorRemoval -
structure
ExactShellGaugeUVStatus -
def
exactShellGaugeUVStatus -
theorem
exactShellGaugeUVStatus_grounded