planeWaveEdgeField_zero_amplitude
plain-language theorem explainer
At zero amplitude the plane-wave edge-length family collapses exactly to the flat background field on the periodic Freudenthal lattice. Anyone computing deficits, second variations, or action profiles along that family cites this identity to anchor at the flat point. The proof is a pointwise funext plus simp using zero-multiplication and add-zero.
Claim. For every polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$ and wavevector $k\in\mathbb{R}^3$, the plane-wave edge field at amplitude $0$ equals the flat edge field on the $N$-periodic lattice: $\ell_{\mathrm{pw}}(E,k;0)=\ell_{\mathrm{flat}}$.
background
This module builds Stage 1 of the Regge TT continuum-symbol program: the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, written as a function of an arbitrary edge squared-length field, together with the plane-wave family used to probe the TT Bloch symbol.
The plane-wave edge field is the one-parameter family that modulates a flat background by a monochromatic wave of amplitude $t$, polarization $E$, and momentum $k$. The flat edge field is the constant (zero-curvature) assignment of squared lengths; it is the base point at which deficits vanish and the true Regge action is zero.
Upstream arithmetic facts used here are the ring identities $0\cdot x=0$ and $x+0=x$ (from the foundation arithmetic layers). The edge index type is the periodic edge set of the Freudenthal lattice of period $N$.
proof idea
Pointwise extensionality on edges, then a single simp that unfolds both the plane-wave family and the flat field. The amplitude factor multiplies the oscillatory term; at amplitude $0$ that product is zero by zero_mul, and adding zero leaves the flat background by add_zero. No geometric lemmas are required.
why it matters
This is the flat-point anchor for the whole plane-wave calculus in the Regge TT preflight. Downstream, deficit_planeWave_zero rewrites deficits along the family at $t=0$ through this identity and the known vanishing of deficits on the flat field; planeWaveActionProfile_zero likewise shows the action profile is zero at amplitude zero by reducing to trueReggeAction on the flat field.
Those facts open the second-variation and TT Bloch-symbol constructions that feed the open continuum target ReggeTTContinuumIsotropyTarget (isotropy of the continuum TT symbol with value $-\frac14 I_{\mathrm{TT}}$). The module sits in the QG full-theory campaign after C10 critic sign-off; this lemma is pure kernel THEOREM scaffolding for that program, not a continuum claim itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.