Encyclopedia Gravity Gravity Analysis One Mode Cylinder Preflight

ARTICLE 5 claims 5 theorems

Gravity Analysis One Mode Cylinder Preflight

A machine-checked check that a single Fourier mode of a frozen energy behaves like a Gaussian, a toy step toward a much larger goal.

Verify this page

The one-mode preflight

In Recognition Science, a ledger is a discrete record of events, and a cost is what recognition must pay. The gravity analysis one mode cylinder preflight is a small, honest module in that framework's machine-checked library of formal theorems. It studies one Fourier mode k on a one-dimensional periodic lattice with N sites, and asks what the frozen quadratic energy of that single mode does as the lattice gets finer. The module does not build a full quantum gravity measure, and it does not claim to. It is a toy check, a preflight, for a candidate approach called C10.

The classical mathematics here is the discrete Laplacian. On the N-site circle, the eigenvalue for mode k is λ_N(k) = 4N² sin²(πk/N). As N grows, this approaches the continuum eigenvalue (2πk)², the eigenvalue of −d²/dx² on the unit circle. The Boltzmann weight for the frozen energy ½λx² is a centered Gaussian with variance v_N(k) = 1/λ_N(k). The module defines this Gaussian explicitly as a probability measure on the real line, using the standard real Gaussian from the Mathlib library. When N is not a multiple of k, the eigenvalue is positive and the Gaussian is non-degenerate; the module works in the range N ≥ 4k to guarantee this.

The theorems proved are genuine statements about this measure. The characteristic function is exp(−v_N t²/2), the second moment equals v_N, and the moment-generating identity holds. The key rate result is uniform in k: |v_N − (2πk)⁻²| ≤ (1/6)/N². This uniformity is not obvious; the naive bound would grow with k, but a lower bound on the eigenvalue cancels that growth. Two convergence statements follow: the second moment tends to (2πk)⁻², and the characteristic function tends pointwise to that of the limiting Gaussian. The module is careful not to claim weak convergence of measures, because the library lacks the Lévy continuity theorem. It also proves the measure is a probability measure for all k and N, including degenerate cases where it becomes a Dirac mass.

In plain language, the module shows that a single Fourier mode of the frozen energy behaves exactly as a physicist would expect: on a fine lattice, its fluctuations are Gaussian with variance 1/(2πk)², and the error shrinks like 1/N² uniformly in k. The word preflight matters. This is a check that the tools work on the simplest possible case, not a step toward a theory of gravity. The module carries no campaign flag, and it is deliberately separate from the Test G lane. It is a foundation stone, verified by machine, on which nothing yet stands.

THEOREM charFun_modeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
charFun_modeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean:159 
/-- TARGET 1 (characteristic function): `charFun μ_N t = exp(−v_N t²/2)`.
Proved from Mathlib's `charFun_gaussianReal` with mean `0`. -/
theorem charFun_modeMeasure (k N : ℕ) (t : ℝ) :
    charFun (modeMeasure k N) t
      = Complex.exp (-(((modeVariance k N : ℝ) : ℂ) * (t : ℂ) ^ 2 / 2)) := by
  unfold modeMeasure
  rw [charFun_gaussianReal]
  congr 1
  push_cast
  ring
THEOREM secondMoment_modeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
secondMoment_modeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean:170 
/-- TARGET 1 (second moment): `∫ x² dμ_N = v_N`. Proved from Mathlib's
`variance_fun_id_gaussianReal` plus the zero-mean identity. -/
theorem secondMoment_modeMeasure (k N : ℕ) :
    ∫ x, x ^ 2 ∂(modeMeasure k N) = ((modeVariance k N : ℝ≥0) : ℝ) := by
  have h := variance_fun_id_gaussianReal (μ := (0 : ℝ)) (v := modeVariance k N)
  rw [variance_eq_integral measurable_id'.aemeasurable] at h
  simp only [integral_id_gaussianReal, sub_zero] at h
  unfold modeMeasure
  exact h
THEOREM modeVarianceReal_rate · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
modeVarianceReal_rate · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean:238 
/-- TARGET 2 (rate): for `k ≥ 1` and `N ≥ 4k`,
`|v_N(k) − (2πk)⁻²| ≤ (1/6)/N²`. The constant `C(k) = 1/6` is uniform
in `k`: `|λ⁻¹ − Λ⁻¹| = |Λ − λ|/(λΛ) ≤ (Λ²/12/N²)/(Λ²/2) = (1/6)/N²`
with `Λ = (2πk)²`, using the Phase-2a expansion for the numerator and
`latticeEigenvalue_lower_bound` for the denominator. -/
theorem modeVarianceReal_rate (k N : ℕ) (hk : 1 ≤ k) (hN : 4 * k ≤ N) :
    |modeVarianceReal k N - (continuumEigenvalue k)⁻¹|
      ≤ 1 / 6 / (N : ℝ) ^ 2 := by
  have hN1 : 1 ≤ N := by omega
  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 hLam_pos : 0 < continuumEigenvalue k := by
    unfold continuumEigenvalue
    have : 0 < 2 * Real.pi * (k : ℝ) := by
      have := Real.pi_pos
      nlinarith
    positivity
  have hlow := latticeEigenvalue_lower_bound k N hk hN
  have hlam_pos : 0 < latticeEigenvalue k N := latticeEigenvalue_pos k N hk hN
  -- Numerator: the Phase-2a expansion, with `(2πk)⁴ = Λ²`.
  have hnum : |continuumEigenvalue k - latticeEigenvalue k N|
      ≤ (continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2 := by
    rw [abs_sub_comm]
    have h4 : (continuumEigenvalue k) ^ 2 = (2 * Real.pi * (k : ℝ)) ^ 4 := by
      unfold continuumEigenvalue
      ring
    rw [h4]
    exact discrete_sine_eigenvalue_expansion k N hN1
  -- Denominator: `λΛ ≥ Λ²/2`.
  have hden : (continuumEigenvalue k) ^ 2 / 2
      ≤ latticeEigenvalue k N * continuumEigenvalue k := by
    have := mul_le_mul_of_nonneg_right hlow hLam_pos.le
    nlinarith [this]
  have hinv : (latticeEigenvalue k N)⁻¹ - (continuumEigenvalue k)⁻¹
      = (continuumEigenvalue k - latticeEigenvalue k N)
        / (latticeEigenvalue k N * continuumEigenvalue k) :=
    inv_sub_inv hlam_pos.ne' hLam_pos.ne'
  unfold modeVarianceReal
  rw [hinv, abs_div, abs_of_pos (mul_pos hlam_pos hLam_pos)]
  calc |continuumEigenvalue k - latticeEigenvalue k N|
        / (latticeEigenvalue k N * continuumEigenvalue k)
      ≤ ((continuumEigenvalue k) ^ 2 / 12 / (N : ℝ) ^ 2)
        / ((continuumEigenvalue k) ^ 2 / 2) :=
        div_le_div₀ (by positivity) hnum (by positivity) hden
    _ = 1 / 6 / (N : ℝ) ^ 2 := by
        field_simp
        ring
THEOREM secondMoment_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
secondMoment_tendsto · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean:298 
/-- TARGET 3 (second moments converge): the actual Gaussian integrals
`∫ x² dμ_N` converge to the continuum mode variance `(2πk)⁻²`. -/
theorem secondMoment_tendsto (k : ℕ) (hk : 1 ≤ k) :
    Filter.Tendsto (fun N : ℕ => ∫ x, x ^ 2 ∂(modeMeasure k N))
      Filter.atTop (nhds ((continuumEigenvalue k)⁻¹)) := by
  refine Filter.Tendsto.congr (fun N => ?_) (modeVarianceReal_tendsto k hk)
  rw [secondMoment_modeMeasure, coe_modeVariance]
THEOREM instIsProbabilityMeasureModeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean
instIsProbabilityMeasureModeMeasure · IndisputableMonolith/Gravity/Analysis/OneModeCylinderPreflight.lean:137 
/-- NON-VACUITY (target 4): `μ_N` is a probability measure for every
`k N`, inherited from Mathlib's `gaussianReal` instance. -/
instance instIsProbabilityMeasureModeMeasure (k N : ℕ) :
    IsProbabilityMeasure (modeMeasure k N) := by
  unfold modeMeasure
  infer_instance

What this page does not claim

This module does not construct a path-sum measure or any field-theoretic measure. This module does not claim weak convergence of measures, only convergence of second moments and characteristic functions pointwise. This module does not support any campaign flag or claim about quantum gravity itself.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND