planeWaveTetVelocity
plain-language theorem explainer
Names the six-component affine velocity of a tetrahedron's local squared-edge coordinates along a polarized plane-wave edge field. Each face velocity is the polarization edge coefficient times the cosine of the Bloch phase at the edge midpoint. Downstream second-variation and TT Bloch-symbol lemmas cite it as the linear coefficient in the affine path through the flat Freudenthal tuple. The body is a direct pointwise product, not a derived identity.
Claim. Given a polarization matrix $E:\{0,1,2\}^2\to\mathbb{R}$, a wave vector $k\in\mathbb{R}^3$, and a periodic tetrahedron $\tau$, the affine velocity of $\tau$'s six local squared-edge coordinates along the plane-wave family is the map $v:\{0,\ldots,5\}\to\mathbb{R}$ with $v_f = c_E(d_f)\,\cos(k\cdot x_{\mathrm{mid}}(f))$, where $d_f$ is the displacement of the $f$-th local edge of $\tau$ and $x_{\mathrm{mid}}(f)$ is that edge's midpoint.
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$, plane-wave edge fields, and existence of the discrete TT Bloch symbol as a normalized second derivative of the nonlinear Regge action at flat.
A periodic tetrahedron carries six local edges. Along the plane-wave family the squared lengths of those edges form a path in $\mathbb{R}^6$. The module proves that path is affine through the canonical Freudenthal flat tuple: $a_\tau(t)=a^*+t,v_\tau$. The coefficient $v_\tau$ is exactly this definition.
The polarization factor $c_E(d)$ is the edge coefficient of the plane-wave field for displacement $d$; the cosine is the real part of the Bloch phase evaluated at the edge midpoint. Gate-0 facts from the derivative-gate import guarantee that at $t=0$ all six squared edges are positive and all dihedral cosines lie in $(-1,1)$, so the flat base point is nondegenerate.
proof idea
Pure definitional construction: for each of the six face indices $f$, look up the local edge of the tetrahedron, read its lattice displacement, multiply the polarization edge coefficient of that displacement by the cosine of the midpoint phase for wave vector $k$, and return the resulting six-tuple. No lemmas are applied; the body is a single lambda.
why it matters
This velocity is the linear data that turns the plane-wave family into an affine path through the Freudenthal flat tetrahedron, which is clause (a) of the module's Gate A1 package. Flat second-variation code builds slot sqrt-derivatives $L'{\tau f}(0)=v{\tau f}/(2\sqrt{a^*f})$ and slot angle derivatives $\theta'{\tau f}(0)=\sum_g v_{\tau g}J_{fg}$ directly from it; those feed the two-jet of the Regge action at flat.
Bloch-interface and assembly layers unfold raw cell stencil terms as products of two such velocities (normalized by flat edge lengths), so the fixed-$N$ TT Bloch symbol identity ultimately packages these coefficients. In the broader Recognition gravity lane this is discrete geometric bookkeeping toward a continuum TT symbol, not a forcing-chain (T0–T8) step; it sits inside the Regge calculus analysis that must close before continuum claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.