continuumProfile_second_deriv
plain-language theorem explainer
Along the wave axis, the continuum Fourier profile of wavenumber k has second derivative equal to -(2πk)² times itself. Anyone citing the flat-torus Lichnerowicz eigenvalue (2πk)² for TT plane waves needs this identity. The proof differentiates the first-derivative formula once more and reduces the complex prefactor via I² = -1.
Claim. For every $k \in \mathbb{N}$ and $t \in \mathbb{R}$, if $u_k$ denotes the continuum profile of wavenumber $k$, then the map $s \mapsto 2\pi i\, k\, u_k(s)$ is differentiable at $t$ with derivative $-(2\pi k)^2 u_k(t)$. Equivalently, $-\partial_t^2 u_k = (2\pi k)^2 u_k$ along the wave direction.
background
This module closes Lane 4 of the Seven-Gaps gravity campaign: operator convergence from a lattice discrete Laplacian to the continuum Lichnerowicz operator on the flat unit 3-torus. Lattice fields are N-periodic maps $\mathbb{Z}\to\mathbb{C}$ (spacing $h=1/N$), not ZMod values, so stencil identities hold pointwise and periodicity supplies the torus.
The continuum profile $u_k$ is the continuous plane-wave mode of integer wavenumber $k$ along one axis of the unit torus (constant in the two transverse coordinates). A prior lemma already gives its first derivative: $\partial_t u_k = 2\pi i k, u_k$. The present result is the second differentiation of that identity.
Scope is deliberately axis-sector only. The module doc warns that Freudenthal stencil energy is anisotropic, so axis stencils must not be read as isotropic recovery of the full Lichnerowicz symbol.
proof idea
Start from the first-derivative lemma continuumProfile_hasDerivAt and multiply the derivative by the constant complex prefactor $2\pi i k$ (HasDerivAt.const_mul). That yields differentiability of $s\mapsto 2\pi i k, u_k(s)$ with derivative equal to $(2\pi i k)^2 u_k(t)$.
An algebraic side goal rewrites the target $-(2\pi k)^2 u_k(t)$ into that same product: after push_cast, a one-line linear_combination against Complex.I_sq (i.e. $I^2=-1$) equates the two complex scalars. Rewrite the goal by that equality and close with the differentiated first-derivative fact.
why it matters
On a Ricci-flat (here flat) background the Lichnerowicz operator on TT perturbations reduces to $-\nabla^2$. For an axial TT plane wave of wavenumber $k$ on the unit 3-torus, the continuum eigenvalue is therefore $(2\pi k)^2$. The module's MODEL block cites this theorem as the proved along-axis half of that claim; transverse derivatives vanish by constancy in $y,z$.
That eigenvalue is the continuum target against which the discrete spectrum (discLap_fourierMode, discreteEigenvalue_tendsto) is compared in the Seven-Gaps operator-convergence lane. No curved-space geometry is formalized: only the flat reduction. Downstream use count is presently zero in the graph, but the definition of the flat Lichnerowicz model eigenvalue is justified by exactly this second-derivative identity.
Framework link: gravity-side spectral control on the recognition lattice, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.