Encyclopedia Gravity Gravity Seven Gaps Exact Shell Gauge Uv
ARTICLE 5 claims 5 theorems
Gravity Seven Gaps Exact Shell Gauge Uv
A machine-checked proof that gravity's path sum can be organized into exact, uncapped shells and made to converge with a hand-inserted regulator, while the physical limit stays open.
The exact shells
In Recognition Science, the path sum for gravity is a sum over discrete complexes: finite collections of vertices, edges, and tetrahedra. The central problem is that this sum is infinite, and the framework needs a principled way to organize it. The Seven Gaps stage in the framework's library provides that organization by grouping complexes into exact complexity shells, where the complexity of a complex is the largest of its counts of vertices, edges, and tetrahedra. This grouping is exact because each complex belongs to exactly one shell, determined by its own signature, with no size cap that could cause the same complex to be counted in multiple shells. This solves a double-counting hazard: earlier bounded classes carried a size cap, so the same abstract complex appeared in every bounded class above its complexity, a cap-dependent artifact that would corrupt any sum over caps.
The framework then proves that the shell-resummed path sum converges when a Gaussian regulator, exp(−ρ·n²), is inserted by hand for every positive regulator strength ρ. This is a mathematical regulator, not derived physics, and the action or phase entering the unitary weight is a parameter, an arbitrary function on equivalence classes, not a derived physical action. The convergence is a theorem: the per-class measure, 1/|Aut|, is well-defined, positive, and at most one; the regulated shell term satisfies a modulus bound; the shell series is summable for every ρ > 0; and the cutoff partial sums converge to the regulated sum. At zero phase, the regulated sum is real and strictly positive, so the result is not vacuous. The shell entropy bound, card (ExactPathClass n) ≤ (n+1)^(12·(n+1)), is also proved, and every shell is inhabited, witnessed by n isolated vertices.
In plain language, the framework establishes a clean, exact bookkeeping for the infinite sum over discrete geometries, and proves that with a hand-inserted regulator the sum converges. What it does not establish is the physical limit: removing the regulator (the ρ → 0⁺ limit) is a named open problem, and the complexity cutoff is not mesh refinement, so nothing here is the physical continuum limit. The framework's library proves the mathematics of the regularized sum; the physics of the regulator's removal remains a target, not a result.
THEOREM shell_index_unique · toExact_relax · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (no double counting).** An exact complex can sit in the
shell at level `n` (i.e. its signature can be a `ShellSig n`) ONLY for
`n = exactComplexity K`: each configuration has exactly one shell.
Combined with the fact that `GlobalEquivalent` lives on a fixed signature,
no abstract complex is counted in two shells. -/
theorem shell_index_unique {v e t : ℕ} (K : ExactComplex v e t) {n : ℕ}
(s : ShellSig n) (hv : sigV s = v) (he : sigE s = e) (ht : sigT s = t) :
n = exactComplexity K := by
unfold exactComplexity
rw [← hv, ← he, ← ht]
exact s.2.symm
/-- **THEOREM (cap-dependence collapses).** Relaxing the cap of a bounded
complex does not change its exact image: the map to the cap-free class
identifies all capped copies of the same configuration (definitional
equality). -/
theorem toExact_relax {B B' : ℕ} (h : B ≤ B') (K : BoundedComplex B) :
toExact (PathSumMeasure.relax h K) = toExact K := rfl
THEOREM exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (shell entropy bound, S1c).** The number of combinatorially
distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`.
Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times
`≤ (n+1)^(6·(n+1))` labeled configurations per signature
(`exactComplex_card_le`, quotient card ≤ labeled card via the surjection
`Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/
theorem exactPathClass_card_le (n : ℕ) :
Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by
have hfiber : ∀ s : ShellSig n,
Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
(n + 1) ^ (6 * (n + 1)) := by
intro s
have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) :=
Nat.card_le_card_of_surjective
(Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s)))
(fun q => Quotient.exists_rep q)
have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤
(n + 1) ^ (6 * (n + 1)) := by
rw [Nat.card_eq_fintype_card]
exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt)
(le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt)
exact le_trans hsurj hlab
rw [Nat.card_sigma]
calc ∑ s : ShellSig n,
Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s)))
≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) :=
Finset.sum_le_sum fun s _ => hfiber s
_ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by
rw [Finset.sum_const, Finset.card_univ, smul_eq_mul]
_ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) :=
Nat.mul_le_mul_right _ (shellSig_card_le n)
_ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add]
_ ≤ (n + 1) ^ (12 * (n + 1)) :=
Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)
THEOREM Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (S2e, non-vacuity).** At zero phase the regulated path sum
has strictly positive real part for every `ρ > 0`: the regulated theory
is not the zero functional. (All terms are nonnegative real and the
`n = 0` term is positive; positivity passes to the `tsum`.) -/
theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) :
0 < (Z_RS_uv ρ zeroPhase).re := by
have hsC : Summable
(fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
(summable_zRSUVShell ρ hρ zeroPhase).congr
(fun n => zRSUVShell_zeroPhase_eq ρ n)
have hsR : Summable
(fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
Complex.summable_ofReal.mp hsC
have hZ : Z_RS_uv ρ zeroPhase =
((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
unfold Z_RS_uv
rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
← Complex.ofReal_tsum]
rw [hZ, Complex.ofReal_re]
exact hsR.tsum_pos
(fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0
(mul_pos (Real.exp_pos _) (shellMass_pos 0))
THEOREM Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (S2e, non-vacuity).** At zero phase the regulated path sum
has strictly positive real part for every `ρ > 0`: the regulated theory
is not the zero functional. (All terms are nonnegative real and the
`n = 0` term is positive; positivity passes to the `tsum`.) -/
theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) :
0 < (Z_RS_uv ρ zeroPhase).re := by
have hsC : Summable
(fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) :=
(summable_zRSUVShell ρ hρ zeroPhase).congr
(fun n => zRSUVShell_zeroPhase_eq ρ n)
have hsR : Summable
(fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) :=
Complex.summable_ofReal.mp hsC
have hZ : Z_RS_uv ρ zeroPhase =
((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by
unfold Z_RS_uv
rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n),
← Complex.ofReal_tsum]
rw [hZ, Complex.ofReal_re]
exact hsR.tsum_pos
(fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0
(mul_pos (Real.exp_pos _) (shellMass_pos 0))
THEOREM exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (shell entropy bound, S1c).** The number of combinatorially
distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`.
Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times
`≤ (n+1)^(6·(n+1))` labeled configurations per signature
(`exactComplex_card_le`, quotient card ≤ labeled card via the surjection
`Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/
theorem exactPathClass_card_le (n : ℕ) :
Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by
have hfiber : ∀ s : ShellSig n,
Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
(n + 1) ^ (6 * (n + 1)) := by
intro s
have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤
Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) :=
Nat.card_le_card_of_surjective
(Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s)))
(fun q => Quotient.exists_rep q)
have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤
(n + 1) ^ (6 * (n + 1)) := by
rw [Nat.card_eq_fintype_card]
exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt)
(le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt)
exact le_trans hsurj hlab
rw [Nat.card_sigma]
calc ∑ s : ShellSig n,
Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s)))
≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) :=
Finset.sum_le_sum fun s _ => hfiber s
_ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by
rw [Finset.sum_const, Finset.card_univ, smul_eq_mul]
_ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) :=
Nat.mul_le_mul_right _ (shellSig_card_le n)
_ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add]
_ ≤ (n + 1) ^ (12 * (n + 1)) :=
Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)
What this page does not claim
The regulator removal limit is not proved; it is a named open problem. The complexity cutoff is not mesh refinement, so this is not the physical continuum limit. The phase entering the path sum is a parameter, not a derived physical action.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- Does the regulated path sum have a finite limit as the regulator strength ρ approaches zero?
- What physical action, if any, does the framework derive for the phase entering the path sum?
- How does the exact shell structure relate to the framework's broader forcing chain for gravity?
- What is the physical interpretation of the regulator, if it is not derived physics?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM shell_index_unique · toExact_relax · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (no double counting).** An exact complex can sit in the shell at level `n` (i.e. its signature can be a `ShellSig n`) ONLY for `n = exactComplexity K`: each configuration has exactly one shell. Combined with the fact that `GlobalEquivalent` lives on a fixed signature, no abstract complex is counted in two shells. -/ theorem shell_index_unique {v e t : ℕ} (K : ExactComplex v e t) {n : ℕ} (s : ShellSig n) (hv : sigV s = v) (he : sigE s = e) (ht : sigT s = t) : n = exactComplexity K := by unfold exactComplexity rw [← hv, ← he, ← ht] exact s.2.symm/-- **THEOREM (cap-dependence collapses).** Relaxing the cap of a bounded complex does not change its exact image: the map to the cap-free class identifies all capped copies of the same configuration (definitional equality). -/ theorem toExact_relax {B B' : ℕ} (h : B ≤ B') (K : BoundedComplex B) : toExact (PathSumMeasure.relax h K) = toExact K := rflEach complex belongs to exactly one shell, determined by its own signature, with no size cap that could cause the same complex to be counted in multiple shells. shell_index_unique · toExact_relax · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.leanTHEOREM exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (shell entropy bound, S1c).** The number of combinatorially distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`. Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times `≤ (n+1)^(6·(n+1))` labeled configurations per signature (`exactComplex_card_le`, quotient card ≤ labeled card via the surjection `Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/ theorem exactPathClass_card_le (n : ℕ) : Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by have hfiber : ∀ s : ShellSig n, Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ (n + 1) ^ (6 * (n + 1)) := by intro s have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) := Nat.card_le_card_of_surjective (Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s))) (fun q => Quotient.exists_rep q) have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤ (n + 1) ^ (6 * (n + 1)) := by rw [Nat.card_eq_fintype_card] exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt) (le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt) exact le_trans hsurj hlab rw [Nat.card_sigma] calc ∑ s : ShellSig n, Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) := Finset.sum_le_sum fun s _ => hfiber s _ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] _ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) := Nat.mul_le_mul_right _ (shellSig_card_le n) _ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add] _ ≤ (n + 1) ^ (12 * (n + 1)) := Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)The shell series is summable for every ρ > 0. exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.leanTHEOREM Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (S2e, non-vacuity).** At zero phase the regulated path sum has strictly positive real part for every `ρ > 0`: the regulated theory is not the zero functional. (All terms are nonnegative real and the `n = 0` term is positive; positivity passes to the `tsum`.) -/ theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) : 0 < (Z_RS_uv ρ zeroPhase).re := by have hsC : Summable (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) := (summable_zRSUVShell ρ hρ zeroPhase).congr (fun n => zRSUVShell_zeroPhase_eq ρ n) have hsR : Summable (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) := Complex.summable_ofReal.mp hsC have hZ : Z_RS_uv ρ zeroPhase = ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by unfold Z_RS_uv rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n), ← Complex.ofReal_tsum] rw [hZ, Complex.ofReal_re] exact hsR.tsum_pos (fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0 (mul_pos (Real.exp_pos _) (shellMass_pos 0))The cutoff partial sums converge to the regulated sum. Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.leanTHEOREM Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (S2e, non-vacuity).** At zero phase the regulated path sum has strictly positive real part for every `ρ > 0`: the regulated theory is not the zero functional. (All terms are nonnegative real and the `n = 0` term is positive; positivity passes to the `tsum`.) -/ theorem Z_RS_uv_zeroPhase_re_pos (ρ : ℝ) (hρ : 0 < ρ) : 0 < (Z_RS_uv ρ zeroPhase).re := by have hsC : Summable (fun n : ℕ => ((Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ)) := (summable_zRSUVShell ρ hρ zeroPhase).congr (fun n => zRSUVShell_zeroPhase_eq ρ n) have hsR : Summable (fun n : ℕ => Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n) := Complex.summable_ofReal.mp hsC have hZ : Z_RS_uv ρ zeroPhase = ((∑' n : ℕ, Real.exp (-ρ * (n : ℝ) ^ 2) * shellMass n : ℝ) : ℂ) := by unfold Z_RS_uv rw [tsum_congr (fun n => zRSUVShell_zeroPhase_eq ρ n), ← Complex.ofReal_tsum] rw [hZ, Complex.ofReal_re] exact hsR.tsum_pos (fun n => (mul_pos (Real.exp_pos _) (shellMass_pos n)).le) 0 (mul_pos (Real.exp_pos _) (shellMass_pos 0))At zero phase, the regulated sum is real and strictly positive. Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.leanTHEOREM exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
/-- **THEOREM (shell entropy bound, S1c).** The number of combinatorially distinct exact complexes of complexity `n` is at most `(n+1)^(12·(n+1))`. Counting audit: `≤ (n+1)³` signature choices (`shellSig_card_le`), times `≤ (n+1)^(6·(n+1))` labeled configurations per signature (`exactComplex_card_le`, quotient card ≤ labeled card via the surjection `Quotient.mk`), and `3 + 6·(n+1) ≤ 12·(n+1)`. -/ theorem exactPathClass_card_le (n : ℕ) : Nat.card (ExactPathClass n) ≤ (n + 1) ^ (12 * (n + 1)) := by have hfiber : ∀ s : ShellSig n, Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ (n + 1) ^ (6 * (n + 1)) := by intro s have hsurj : Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) := Nat.card_le_card_of_surjective (Quotient.mk (exactSetoid (sigV s) (sigE s) (sigT s))) (fun q => Quotient.exists_rep q) have hlab : Nat.card (ExactComplex (sigV s) (sigE s) (sigT s)) ≤ (n + 1) ^ (6 * (n + 1)) := by rw [Nat.card_eq_fintype_card] exact exactComplex_card_le n _ _ _ (le_of_lt s.1.1.isLt) (le_of_lt s.1.2.1.isLt) (le_of_lt s.1.2.2.isLt) exact le_trans hsurj hlab rw [Nat.card_sigma] calc ∑ s : ShellSig n, Nat.card (Quotient (exactSetoid (sigV s) (sigE s) (sigT s))) ≤ ∑ _s : ShellSig n, (n + 1) ^ (6 * (n + 1)) := Finset.sum_le_sum fun s _ => hfiber s _ = Fintype.card (ShellSig n) * (n + 1) ^ (6 * (n + 1)) := by rw [Finset.sum_const, Finset.card_univ, smul_eq_mul] _ ≤ (n + 1) ^ 3 * (n + 1) ^ (6 * (n + 1)) := Nat.mul_le_mul_right _ (shellSig_card_le n) _ = (n + 1) ^ (3 + 6 * (n + 1)) := by rw [← pow_add] _ ≤ (n + 1) ^ (12 * (n + 1)) := Nat.pow_le_pow_right (Nat.succ_pos n) (by omega)The shell entropy bound, card (ExactPathClass n) ≤ (n+1)^(12·(n+1)), is proved. exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean