Gravity Seven Gaps Exact Shell Gauge Uv Z Rs Uv Zero Phase Re Pos

The zero-phase sum

A ledger in Recognition Science is a discrete record of events. Here the events are finite combinatorial complexes: vertices, edges, and tetrahedra. The declaration Z_RS_uv_zeroPhase_re_pos is a theorem in the framework's machine-checked library of formal theorems. It states that when the phase assigned to every complex is zero, the regulated sum over all such complexes, Z_RS_uv, has a real part that is strictly greater than zero.

The sum is not over all complexes at once. It is organized into shells, where shell n contains exactly those complexes whose complexity, the largest of the counts of vertices, edges, and tetrahedra, equals n. Each complex is counted once, because the shell index is determined by the complex itself, not by an external size cap. Each shell is finite, and the measure assigned to a complex is the reciprocal of the size of its automorphism group, a standard symmetry-factor convention in discrete gravity. The regulator is a Gaussian factor exp(-ρ·n²) that multiplies each shell term, with strength ρ > 0.

The theorem Z_RS_uv_zeroPhase_re_pos proves that for every positive ρ, the real part of the regulated sum is positive. This is a non-vacuity result: the sum does not vanish or become negative at zero phase. It is a proved statement in the library, with no unproved axioms beyond the standard three.

What the theorem does not claim is as important as what it proves. The Gaussian regulator is a mathematical insertion, not derived physics. The phase function is a parameter, not a physical action. The limit as ρ approaches zero from above, which would remove the regulator, is a named open problem, not a proved result. The physical continuum limit, where the complexity cutoff would correspond to mesh refinement, is also open. The theorem is a statement about a regularized, model-dependent sum, not about the physical world.

/-- **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 complexity of an exact complex: determined by its signature alone. -/
def exactComplexity {v e t : ℕ} (_ : ExactComplex v e t) : ℕ :=
  max v (max e t)

/-- The symmetry-factor measure of an exact labeled complex:
`μ(K) = 1/|Aut K|` (MODEL: the standard discrete-gravity convention). -/
noncomputable def exactMu {v e t : ℕ} (K : ExactComplex v e t) : ℝ :=
  1 / (Nat.card (ExactAut K) : ℝ)

What this page does not claim

The Gaussian regulator is derived from physics. The limit as ρ approaches zero from above exists. The complexity cutoff corresponds to mesh refinement. The phase function is a 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: