Encyclopedia Gravity Gravity Seven Gaps Exact Shell Gauge Uv Exact Shell Gauge Uvstatus Grounded

ARTICLE 5 claims 4 theorems 1 model

Gravity Seven Gaps Exact Shell Gauge Uv Exact Shell Gauge Uvstatus Grounded

A machine-checked ledger sorts discrete geometries into exact complexity classes and proves the sum over them converges when damped, without claiming the damping is physics.

Verify this page

The shell ledger

The declaration exactShellGaugeUVStatus_grounded is a status record inside the Recognition Science framework's machine-checked library of formal theorems. It organizes a path-sum over discrete geometries, the kind of sum a quantum gravity theory might use, into exact complexity shells. A shell is a collection of all geometries sharing the same complexity index, where complexity is the largest of three counts: vertices, edges, and tetrahedra. The key structural result is that this classification is exact: every geometry belongs to exactly one shell, with no size cap and no double counting.

The framework proves several theorems about these shells. Each shell is finite, inhabited, and has a size bounded by (n+1)^(12(n+1)). The measure on each shell is the symmetry factor 1/|Aut|, the standard convention in discrete gravity. The central analytic result is that the shell-resummed path sum with an explicit Gaussian regulator exp(-ρ·n²) converges for every positive regulator strength ρ. At zero phase, the sum is real and strictly positive, so the construction is not vacuous.

In Recognition Science, this is a step toward a discrete path integral for gravity. The framework models the path sum as a sum over equivalence classes of finite simplicial complexes under relabeling. The regulator is a mathematical device inserted by hand to make the sum converge; it is not derived from any physical principle. The action or phase entering the sum is likewise a parameter, an arbitrary function on equivalence classes, not a derived physical action.

What the declaration does not claim is as important as what it proves. It does not claim that removing the regulator, taking the ρ → 0⁺ limit, yields a finite result; that limit is a named open problem. It does not claim that this discrete sum is the physical continuum limit of gravity; the complexity cutoff is not mesh refinement, and the continuum limit remains an open target. The module flips no flags in the framework's full theory ledger.

The practical consequence is a clean, finite, and well-defined object: a convergent sum over all discrete geometries, organized by exact complexity, with a symmetry-factor measure. This gives the framework a concrete starting point for further analysis, even though the physical interpretation and the continuum limit remain open.

THEOREM instFintypeExactPathClass · exactPathClass_unbounded_support · exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
instFintypeExactPathClass · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:326 
/-- **THEOREM (S1b).**  Each exact complexity shell is a finite type. -/
noncomputable instance instFintypeExactPathClass (n : ℕ) :
    Fintype (ExactPathClass n) :=
  Fintype.ofFinite _
exactPathClass_unbounded_support · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:427 
/-- **THEOREM (S1d, unbounded support).**  EVERY shell is inhabited: the
`n`-isolated-vertices complex has complexity exactly `n`, so no shell is
eventually empty. -/
theorem exactPathClass_unbounded_support (n : ℕ) :
    0 < Nat.card (ExactPathClass n) :=
  Nat.card_pos
exactPathClass_card_le · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:368 
/-- **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
Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:764 
/-- **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
Z_RS_uv_zeroPhase_re_pos · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:764 
/-- **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 shell_index_unique · toExact_relax · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
shell_index_unique · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:337 
/-- **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
toExact_relax · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:355 
/-- **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
MODEL Z_RS_uv · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean
Z_RS_uv · IndisputableMonolith/Gravity/SevenGaps/ExactShellGaugeUV.lean:714 
/-- **The Gaussian-UV-regularized recognition path sum (S2d).**  The full
shell series at regulator strength `ρ`.  Well-defined as a `tsum`; for
`ρ > 0` the series is summable (`summable_zRSUVShell`), so this is the
genuine limit of the cutoff partial sums (`zRSUVCutoff_tendsto`). -/
noncomputable def Z_RS_uv (ρ : ℝ) (phase : ∀ n : ℕ, ExactPathClass n → ℝ) :
    ℂ :=
  ∑' n : ℕ, zRSUVShell ρ phase n

What this page does not claim

The regulator removal limit ρ → 0⁺ exists. The discrete sum is the physical continuum limit of gravity. The action or phase in the sum is derived physics.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND