Gravity Seven Gaps Exact Shell Gauge Uv Z Rsuvshell Zero Phase Eq

The zero-phase sum

A path sum in physics adds up contributions from every possible history of a system. In discrete gravity, the histories are combinatorial objects: collections of vertices, edges, and tetrahedra. The Recognition Science framework organizes these into complexity shells, grouping all configurations with the same size. The declaration zRSUVShell_zeroPhase_eq concerns the simplest possible weighting, called zero phase, where every configuration contributes with phase zero, meaning no oscillating factor at all.

With zero phase, the framework's library proves a concrete fact: the regulated sum Z_RS_uv is real and strictly positive for every positive regulator strength ρ. The regulator is a Gaussian factor exp(−ρ·n²) that suppresses large shells, making the infinite sum converge. The theorem Z_RS_uv_zeroPhase_re_pos states that the real part of this sum is greater than zero. This is not a vacuous result: it shows the sum is well-behaved and nonzero, a necessary sanity check for any path-sum construction.

The positivity proof rests on a chain of earlier results. Each shell has finitely many configurations, and each configuration carries a symmetry weight 1/|Aut|, the reciprocal of the number of its automorphisms. The shell mass, the sum of these weights, is positive for every shell. The regulated shell terms are summable, and the partial sums converge to the full sum. The zero-phase result then follows from the positivity of every term.

What the declaration does not claim is equally important. The Gaussian regulator is a mathematical device inserted by hand; it is not derived from physics. The phase function is an arbitrary parameter, not a physical action. The limit ρ → 0⁺, removing the regulator, is a named open problem, recorded as HasZRSRegulatorRemoval with status false. Nothing here is a physical continuum limit: the complexity cutoff is not mesh refinement. The result is a theorem about a regularized mathematical object, not a physical prediction.

/-- **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 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.**  Every shell carries strictly positive measure (the shell
is inhabited by `isolatedClass n` and each class has `μ > 0`). -/
theorem shellMass_pos (n : ℕ) : 0 < shellMass n :=
  Finset.sum_pos (fun c _ => classMu_pos c) Finset.univ_nonempty

What this page does not claim

The Gaussian regulator is derived physics. The regulator removal limit ρ → 0⁺ exists. The complexity cutoff is a physical continuum limit or mesh refinement.

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: