Gravity Analysis One Mode Cylinder Preflight Lattice Eigenvalue Nonneg

A single mode's energy

In the mathematics of vibrating strings and heat flow, a common move is to replace a continuous circle with a finite ring of N equally spaced points. A wave on the circle, like e^(2πikx), has a known energy of (2πk)². On the discrete ring, the same wave has an energy given by the formula λ_N(k) = 4N² sin²(πk/N). This quantity is the discrete Hessian eigenvalue for Fourier mode k on the N-site periodic lattice.

The declaration latticeEigenvalue_nonneg proves, in the machine-checked library of formal theorems, that this discrete energy is always greater than or equal to zero, for every mode k and every lattice size N. The proof is immediate: the formula is a product of squares, and squares are never negative. The result is tagged THEOREM, meaning it is axiom-clean and carries no unproven assumptions.

This non-negativity is the load-bearing floor for everything else in the module. Because the eigenvalue is never negative, its reciprocal, the variance v_N(k) = 1/λ_N(k), is also never negative. That variance defines a centered Gaussian probability measure on the real line, the one-mode cylinder measure. The non-negativity guarantee is what lets the framework treat this measure as a genuine probability distribution rather than a formal artifact.

In Recognition Science, this one-mode toy preflight is a deliberately small step. It does not construct a field-theoretic measure, does not flip any campaign flag, and does not claim weak convergence of measures. The classical Lévy continuity theorem would upgrade the pointwise convergence of characteristic functions to weak convergence, but that upgrade is not available in the current library and is not claimed here. The module proves honest statements about the real Gaussian measure, scoped to N ≥ 4k where the eigenvalue is strictly positive and the measure is non-degenerate.

What the declaration changes is the ground state of a larger calculation. It certifies that the discrete energy spectrum has no negative modes, so the frozen quadratic energy is bounded below. That boundedness is what makes the Gaussian measure well-defined in the first place. The small fact is the foundation stone for the rate of convergence and the moment identities that follow, and those in turn are the preflight data for a candidate measure that remains open.

/-- `λ_N(k) ≥ 0` always (it is `4N²` times a square). -/
theorem latticeEigenvalue_nonneg (k N : ℕ) : 0 ≤ latticeEigenvalue k N := by
  unfold latticeEigenvalue
  positivity

/-- `v_N(k) ≥ 0` always. -/
theorem modeVarianceReal_nonneg (k N : ℕ) : 0 ≤ modeVarianceReal k N :=
  inv_nonneg.mpr (latticeEigenvalue_nonneg k N)

/-- In scope (`k ≥ 1`, `N ≥ 4k`) the eigenvalue is strictly positive. -/
theorem latticeEigenvalue_pos (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
    0 < latticeEigenvalue k N := by
  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
  have hLam : 0 < continuumEigenvalue k := by
    unfold continuumEigenvalue
    have : 0 < 2 * Real.pi * (k : ℝ) := by
      have := Real.pi_pos
      nlinarith
    positivity
  linarith [latticeEigenvalue_lower_bound k N hk hN]

/-- NON-VACUITY (target 4): in scope `μ_N` is a genuinely non-degenerate
Gaussian (not the Dirac mass): its `ℝ≥0` variance parameter is
nonzero. -/
theorem modeVariance_ne_zero (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
    modeVariance k N ≠ 0 := by
  have hpos := modeVarianceReal_pos k N hk hN
  simp only [modeVariance, ne_eq, Real.toNNReal_eq_zero, not_le]
  exact hpos

What this page does not claim

This declaration does not construct a field-theoretic measure. This declaration does not claim weak convergence of the one-mode measures. This declaration does not flip any campaign flag or support any claim about the full gravity theory.

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/Analysis/OneModeCylinderPreflight.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: