Gravity Analysis One Mode Cylinder Preflight Mode Variance Real Nonneg

A variance that stays nonnegative

In the study of random fluctuations, the variance of a probability distribution measures how spread out its values are. For a centered Gaussian distribution, the variance is the single number that completely describes its width: it is the expected value of the square of the deviation from the mean. A variance can never be negative, because it is an average of squared quantities. The declaration modeVarianceReal_nonneg is a formal, machine-checked proof that a specific variance, defined in the Recognition Science framework, always obeys this fundamental property.

The variance in question belongs to a single Fourier mode on a discretized circle. The framework models a one-dimensional periodic lattice of N sites, and considers a single oscillatory mode with integer wavenumber k. The energy of this mode is a quadratic function of its amplitude, and the coefficient of that quadratic term is called the lattice eigenvalue. The variance is defined as the reciprocal of this eigenvalue, a standard relationship in statistical mechanics where the width of thermal fluctuations is inversely proportional to the stiffness of the potential. The declaration proves that this reciprocal, called modeVarianceReal (a real number representing the variance), is always greater than or equal to zero for every choice of wavenumber k and lattice size N.

The proof is short and rests on the fact that the lattice eigenvalue itself is nonnegative. This eigenvalue is given by the formula 4N² sin²(πk/N), which is a product of squares and therefore never negative. The framework's library of formal theorems contains a proof of this nonnegativity, and the theorem about the variance follows directly by taking the reciprocal of a nonnegative number. The result is a genuine statement about a standard mathematical object, the real Gaussian measure, and is not a symbolic placeholder or an unproven assumption.

What this declaration does not claim is more interesting than what it does. It does not assert that the variance is positive, only that it is nonnegative. The variance can be zero, and in fact it is zero at certain degenerate resolutions where the lattice eigenvalue vanishes. The framework carefully separates these cases: a separate theorem, with additional conditions, proves that the variance is strictly positive when the lattice is fine enough relative to the wavenumber. This declaration also says nothing about the limit of the variance as the lattice becomes infinitely fine; that is the subject of a different convergence theorem. It is a single, simple, but essential brick in a larger structure, ensuring that a basic physical quantity has the correct sign.

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

/-- One-mode Gaussian variance in lattice units: `v_N(k) = λ_N(k)⁻¹`
(junk value `0` at degenerate resolutions, by Lean's `0⁻¹ = 0`). -/
def modeVarianceReal (k N : ℕ) : ℝ := (latticeEigenvalue k N)⁻¹

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

What this page does not claim

The variance is always positive, only that it is never negative. This declaration says anything about the convergence of the variance as the lattice size tends to infinity. This result is part of the construction of a full field-theoretic measure or carries any weight for a campaign flag.

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: