Gravity Analysis One Mode Cylinder Preflight Lattice Eigenvalue Pos

A positive eigenvalue

The declaration latticeEigenvalue_pos is a formal theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a single Fourier mode k on a one-dimensional periodic lattice with N sites, a toy model used to study how a continuous system emerges from a discrete one. The theorem states that for any mode k ≥ 1 and any lattice with N ≥ 4k sites, the discrete Hessian eigenvalue λ_N(k) = 4N² sin²(πk/N) is strictly positive. This eigenvalue is the curvature of a frozen quadratic energy, and its positivity means the energy function is convex, not flat or saddle-shaped, at that mode.

The proof is short and relies on a comparison: the discrete eigenvalue is at least half the continuum eigenvalue (2πk)², which is itself positive. The condition N ≥ 4k ensures the lattice is fine enough to resolve the mode; at coarser resolutions the eigenvalue can vanish, and the statement deliberately excludes those cases. The theorem is one of several in the module that together establish that the Gaussian measure built from this eigenvalue is a genuine, non-degenerate probability distribution, not a Dirac mass. This matters because the measure is the building block for a statistical model of a quantum field, and a degenerate measure would make the model trivial.

In Recognition Science, this theorem is a preflight check: it verifies a technical prerequisite before any larger claim is attempted. It does not construct a field-theoretic measure, does not prove weak convergence of the measures, and does not assign any physical meaning to the eigenvalue beyond its role in the toy model. The theorem is a statement about a single Fourier mode, not about the full quantum gravity theory the framework aims to build. Its value is that it removes one potential obstruction, showing that the discrete model is well-behaved in the regime where it is intended to approximate the continuum.

The practical consequence is that the statistical model is well-defined: the variance of the Gaussian is finite and positive, so the measure has a meaningful second moment. This is a necessary condition for the model to be usable, but it is far from sufficient. The theorem does not say that the model is correct, that it converges to a known quantum field theory, or that it predicts any observable. It is a small but solid step, one that the framework's library records as a formal theorem with no unproven assumptions.

What the theorem does not claim is as important as what it does. It does not claim that the discrete eigenvalue equals the continuum one; it only bounds the difference. It does not claim that the measure converges weakly; the library lacks the Lévy continuity theorem, so only pointwise convergence of characteristic functions is proved. And it does not claim that the model is physical; that would require a separate argument connecting the toy to the full theory. The theorem is a precise, limited statement, and the framework's honesty about its scope is part of its method.

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

/-- Eventual eigenvalue lower bound: for `k ≥ 1` and `N ≥ 4k`,
`λ_N(k) ≥ (2πk)²/2`. Derived from the Phase-2a expansion: the error
`((2πk)⁴/12)/N²` is at most `(2πk)²/2` once `(2πk)² ≤ 6N²`, which
`π ≤ 4` and `N ≥ 4k` guarantee. This is what keeps `λ_N(k)⁻¹`
controlled in the rate bound. -/
theorem latticeEigenvalue_lower_bound (k N : ℕ) (hk : 1 ≤ k)
    (hN : 4 * k ≤ N) :
    continuumEigenvalue k / 2 ≤ latticeEigenvalue k N := by
  have hN1 : 1 ≤ N := by omega
  have hexp := discrete_sine_eigenvalue_expansion k N hN1
  have hkR : (1 : ℝ) ≤ (k : ℝ) := by exact_mod_cast hk
  have hNR : (4 : ℝ) * (k : ℝ) ≤ (N : ℝ) := by exact_mod_cast hN
  have hNpos : (0 : ℝ) < (N : ℝ) := by linarith
  have hpi2 : Real.pi * Real.pi ≤ 16 := by
    nlinarith [Real.pi_le_four, Real.pi_pos]
  have hN2 : 16 * (k : ℝ) ^ 2 ≤ (N : ℝ) ^ 2 := by nlinarith [hkR, hNR]
  have h1 : (2 * Real.pi * (k : ℝ)) ^ 2 ≤ 6 * (N : ℝ) ^ 2 := by
    nlinarith [hpi2, hN2, sq_nonneg (k : ℝ),
      mul_nonneg (by linarith : (0 : ℝ) ≤ 16 - Real.pi * Real.pi)
        (sq_nonneg (k : ℝ))]
  have h12 : (0 : ℝ) < 12 * (N : ℝ) ^ 2 := by positivity
  have hkey : (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2
      ≤ (2 * Real.pi * (k : ℝ)) ^ 2 / 2 := by
    rw [div_div, div_le_iff₀ h12]
    nlinarith [h1, sq_nonneg (2 * Real.pi * (k : ℝ))]
  have habs := abs_le.mp hexp
  unfold continuumEigenvalue latticeEigenvalue
  linarith [habs.1, hkey]

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

The theorem does not construct a field-theoretic measure or any path-sum measure. The theorem does not prove weak convergence of the measures. The theorem does not assign physical meaning to the eigenvalue beyond the toy model.

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: