waveNormSq_preflight_eq_identity
plain-language theorem explainer
The squared Euclidean wave-covector norm from the 4D continuum preflight is definitionally identical to the same norm in the exact midpoint m² TT-identity module. Anyone equating Rayleigh quotients or residual faces across those modules cites this glue. The proof is pure reflexivity: both sides expand to the same four-term sum of squares.
Claim. For every real 4-wave covector $k\in\mathbb{R}^4$, the squared Euclidean norm $\sum_{i=0}^{3} k_i^2$ as defined in the continuum preflight equals the same sum as defined in the exact midpoint $m^2$ TT-identity module.
background
This module sits in the QG full-theory campaign at the Recognition gate of the 4D continuum closure. It builds a canonical Recognition mesh on the periodic Freudenthal 4-torus and attaches a value-level action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol on that torus family.
A wave covector Wave4 is a real 4-tuple (one component per spacetime direction on the lattice). Both the continuum preflight and the exact midpoint m² TT-identity packages define its squared Euclidean norm by the same formula: sum of squares of the four components. Downstream Rayleigh identities and residual-face statements need to move non-vanishing hypotheses and normalizations between those two namespaces without changing the real number.
The preferred limit shape in this bridge is amplitude Hessian at fixed mesh, then $N\to\infty$. Arbitrary test-variation pullbacks are excluded by the preflight; the nonlinear Schläfli lift of the Hessian remains open.
proof idea
One-line reflexivity. Both waveNormSq definitions unfold to $\sum_{i:\mathrm{Fin},4} k_i\cdot k_i$ on the same Wave4 carrier (an abbrev of the preflight wave type), so Lean closes the equality by rfl with no rewriting or lemmas.
why it matters
Tiny definitional bridge, but it is the seam that lets Rayleigh and residual arguments treat preflight norms and midpoint-identity norms as interchangeable. Downstream it feeds the closed Recognition-mesh midpoint convergence at the scale-explicit Option-C EH face and the pure-gauge vanishing face (recognitionExactJConvergesEH_closed, recognitionExactJConvergesGaugeZero_closed). The same glue appears in the exact midpoint Bloch m² Rayleigh identities that pin the unit-Frobenius TT face to $-1/8$ and the pure-gauge face to $0$, and in the typed residual Option-C faces of the SRS→EH 4D package.
Within the campaign honesty bounds this does not flip gap_action_recovery, does not inhabit S_RS_converges_EH_4d, and does not elevate the Hessian to the full nonlinear Regge action via Schläfli. It only licenses norm transport so those value-level continuum faces can be stated once.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.