planeWaveTetSqEdges_zero
plain-language theorem explainer
At vanishing amplitude the plane-wave edge field on any periodic tetrahedron recovers exactly the flat Freudenthal squared-edge 6-tuple. Gate A1 smoothness and second-variation arguments cite this as the base point of the affine path. The proof is a short rewrite of the affine formula at t=0 via zero-multiplication and add-zero.
Claim. For every polarization matrix $E:\mathbb{R}^{3\times 3}$, wave covector $k$, and periodic tetrahedron $\tau$ on the $N$-torus, the local squared-edge 6-tuple of the plane-wave edge field at amplitude $t=0$ equals the flat Freudenthal squared-edge tuple.
background
This module is Gate A1 of the Normalization-Gated Schläfli Two-Jet protocol in the Regge TT continuum-symbol program: fixed lattice size $N$, true nonlinear Regge action, plane-wave family of edge fields. The family is parameterized by amplitude $t\in\mathbb{R}$, polarization $E$, and wave vector $k$; each tetrahedron carries a local squared-edge 6-tuple obtained by restricting the edge field.
Upstream, the Freudenthal cube triangulation supplies a canonical flat 6-tuple of squared edge lengths (all positive, Cayley-Menger determinant $cm_3=8>0$, cosines strictly inside $(-1,1)$). The companion lemma that the path is affine, $t\mapsto\mathrm{flat}+t\cdot v$, names the velocity coefficients and evaluates the field at general $t$. Arithmetic identities $0\cdot v=0$ and $x+0=x$ then pin the $t=0$ slice.
Local theoretical setting: prove that every tetrahedron's squared-edge path is affine through the flat point, so dihedral angles and the action profile $S(t)$ are $C^n$ at $t=0$, unlocking the fixed-$N$ TT Bloch symbol as $S''(0)$.
proof idea
Term-mode, three steps. Extensionality on the six edge slots of the tetrahedron reduces the 6-tuple equality to a pointwise claim. Rewrite by the affine evaluation lemma (squared edges equal flat plus $t$ times the named velocity). Specialize $t=0$: zero-multiplication kills the velocity term and add-zero leaves the flat Freudenthal tuple.
why it matters
This is clause (b) of Gate A1: the plane-wave path sits exactly on the nondegenerate flat Freudenthal point at $t=0$. Downstream, the dihedral-angle smoothness theorem composes the angle map's $\mathrm{ContDiffAt}$ at that flat 6-tuple with the affine path. Flat-second-variation uses it to show the zero amplitude is path-good (positive edges, interior cosines), that goodness persists in a neighborhood, and that each slot-angle derivative at flat equals the flat Jacobian contraction.
Together these feed the fixed-$N$ existence of the TT Bloch symbol: $S(t)$ is $C^2$ at $0$, so the centered second difference converges to $S''(0)$, identified with the symbol. No continuum limit or global $C^4$ hypothesis is required. Framework role is pure gravity analysis on the discrete Regge side, not a T0-T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.