continuumEigenvalue
plain-language theorem explainer
Defines the continuum Fourier eigenvalue Λ(k)=(2πk)² for mode k on the unit circle, the −d²/dx² eigenvalue of e^{2πikx}. Gravity analysts cite it as the N→∞ target of the discrete Hessian λ_N(k)=4N²sin²(πk/N) in the one-mode cylinder preflight. The body is a one-line arithmetic definition, not a proved identity.
Claim. For each natural number $k$, the continuum eigenvalue is $\Lambda(k) := (2\pi k)^2$, i.e. the eigenvalue of $-\frac{d^2}{dx^2}$ on the complex exponential $e^{2\pi i k x}$ over the unit-length circle.
background
This module is a one-mode toy preflight for candidate C10 (Gaussian cylinder-measure limit of a frozen quadratic energy). It studies a single Fourier mode $k$ on the $N$-site periodic lattice of the unit circle (spacing $1/N$), not a path-sum or field-theoretic measure, and carries no campaign flag weight.
The discrete Hessian eigenvalue in lattice units is $\lambda_N(k) := 4N^2\sin^2(\pi k/N)$. Its quantitative continuum expansion $|\lambda_N(k)-(2\pi k)^2|\le((2\pi k)^4/12)/N^2$ is already proved in SpectralConvergence.discrete_sine_eigenvalue_expansion. The continuum target of that expansion is exactly $\Lambda(k)=(2\pi k)^2$, the classical $-d^2/dx^2$ eigenvalue of $e^{2\pi ikx}$ on the unit circle.
The Boltzmann weight of the frozen quadratic $\tfrac12\lambda x^2$ is the centered Gaussian of variance $v_N(k)=\lambda_N(k)^{-1}$. All later rate, positivity, and characteristic-function statements compare $v_N$ (or $\lambda_N$) against powers of this continuum eigenvalue.
proof idea
Pure definition: the right-hand side is the elementary real expression $(2\cdot\pi\cdot k)^2$. No lemmas, tactics, or axioms are involved. Downstream proofs unfold the name and use elementary positivity of $2\pi k$ for $k\ge 1$.
why it matters
This constant is the continuum anchor for the whole one-mode preflight. It appears in the eigenvalue lower bound $\lambda_N(k)\ge\Lambda(k)/2$ (for $N\ge 4k$), which keeps inverses controlled; in the strict positivity of $\lambda_N$ and of the limiting variance $\Lambda(k)^{-1}$; in the uniform rate $|v_N(k)-\Lambda(k)^{-1}|\le(1/6)/N^2$; in the variance limit $v_N\to\Lambda(k)^{-1}$; and in the pointwise characteristic-function limit $\mathrm{charFun}(\mu_N,t)\to\exp(-\Lambda(k)^{-1}t^2/2)$.
Those targets are the Mathlib-level content of the C10 preflight (Gaussian cylinder limit for one frozen mode). The definition itself is classical spectral geometry; its role here is to name the $N\to\infty$ object against which lattice quantities are measured. It does not touch the Recognition forcing chain (T0–T8), RCL, or the mass ladder; it is local analytic scaffolding for the gravity analysis lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.