continuumProfile
plain-language theorem explainer
Defines the continuum axis plane-wave profile t ↦ exp(2π i k t) on the unit circle, valued in ℂ. Gravity and spectral analysts cite it as the continuum reference mode against which the discrete Fourier eigenvalue on the flat 3-torus is compared. The body is a direct Complex.exp of the linear phase.
Claim. For each wave number $k \in \mathbb{N}$ and real coordinate $t$, the continuum profile is the complex plane wave $\mathrm{continuumProfile}(k,t) := \exp(2\pi i k t)$.
background
The module treats Lane 4 of the Seven-Gaps campaign: operator convergence of a discrete Lichnerowicz-type spectrum on the flat unit 3-torus toward the continuum operator. Lattice functions are N-periodic maps $\mathbb{Z}\to\mathbb{C}$ with spacing $h=1/N$, not functions on $\mathrm{ZMod},N$, so stencil identities hold pointwise and periodicity alone supplies the torus reading.
Scope is deliberately axis-sector only: modes $k=(k,0,0)$ under the componentwise axis stencil. A prior Freudenthal-stencil preflight showed the continuum moment tensor of the frozen quadratic energy is anisotropic, so axis results must not be read as isotropic full-spectrum recovery.
The continuum profile is the 1D building block for those axis modes: pure monochromatic phase along the wave axis, constant in the transverse directions once lifted to a 3-torus TT plane wave.
proof idea
Pure definition: the value is Complex.exp of the complexified linear phase $2\pi i k t$. No lemmas, no tactics; noncomputable only because complex exponential is noncomputable in Mathlib.
why it matters
Feeds three immediate parents in the same file: the continuum TT plane wave on the unit 3-torus (axis mode), obtained by scaling a polarization matrix by this profile; the first-derivative theorem giving factor $2\pi i k$ times the profile; and the second-derivative theorem identifying $-(2\pi k)^2$ as the genuine $-d^2/dt^2$ eigenvalue along the wave direction.
Those derivative facts are the continuum side of the discrete-to-continuum eigenvalue comparison that closes the operator-convergence gap on the flat torus. Within Recognition Science gravity this is scaffolding for matching lattice TT spectra to continuum Lichnerowicz eigenvalues under the axis stencil, not a claim about curved backgrounds or full isotropic recovery (C10/P-iso remains open).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.