Gravity Seven Gaps Exact Shell Gauge Uv Exists Gaussian Domination

The Gaussian-regulated sum

In the Recognition Science framework, a path sum is a way of adding up contributions from all possible discrete spacetime configurations, much as a partition function in statistical mechanics sums over all microstates. The declaration exists_gaussian_domination establishes a precise convergence result for such a sum. The configurations are organized into exact complexity shells, where each shell contains all configurations sharing the same maximum of three counts: vertices, edges, and tetrahedra. The sum is then regulated by multiplying each shell's contribution by a Gaussian factor exp(−ρ·n²), where n is the shell index and ρ is a positive real number. The theorem proves that for every positive ρ, this regulated sum converges to a finite complex number.

The proof rests on a series of machine-checked steps. Each shell is a finite set, and the number of configurations in shell n is bounded by (n+1)^(12·(n+1)). Each configuration within a shell carries a weight equal to 1 divided by the size of its automorphism group, a standard symmetry factor in discrete gravity. The theorem shows that the per-shell contribution obeys a modulus bound, which makes the entire series summable for any ρ > 0. At zero phase, where every configuration contributes with phase zero, the regulated sum is real and strictly positive, confirming the construction is non-vacuous. The library also proves that each shell is nonempty, containing at least the configuration of n isolated vertices.

The motivation for this construction is to avoid a double-counting problem. Earlier bounded-complex path sums carried a size cap, so the same abstract complex appeared in every cap above its complexity. The exact shells have no cap: a configuration's signature (v, e, t) determines exactly one shell index, max(v, max(e, t)), so no configuration is counted twice. This is the key structural improvement the declaration formalizes.

In Recognition Science, this result is a theorem about a mathematical object, not a statement about physical gravity. The Gaussian regulator is inserted by hand; it is not derived from any physical principle. The action or phase entering the sum is an arbitrary parameter, not a derived quantity. The limit ρ → 0⁺, which would remove the regulator, is a named open problem, not a proved statement. The physical continuum limit, where the complexity cutoff would correspond to mesh refinement, is also not established. The declaration flips no flag in the full theory ledger; it is a standalone mathematical convergence result.

What the result changes is the mathematical setting: it provides a well-defined, finite object that can be studied further. The convergence is a necessary first step for any future attempt to make sense of the path sum. But it does not by itself give the sum a physical interpretation, and it does not connect the discrete configurations to continuous spacetime. Those steps remain targets for future work.

/-- **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

/-- **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 (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

/-- **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 (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

What this page does not claim

The Gaussian regulator is derived from physics; it is inserted by hand as a mathematical device. The limit as ρ approaches zero exists; regulator removal is a named open problem. The discrete configurations correspond to continuous spacetime; the physical continuum limit is not established. The sum has a physical interpretation as a gravitational path integral; only its mathematical convergence is proved.

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: