waveNormSq
plain-language theorem explainer
Squared Euclidean norm of a real 4-covector on the Freudenthal 4-torus: sum of squares of its four components. Gravity analysts cite it whenever a continuum or discrete Regge symbol must be normalized by |k|², or when TT and pure-gauge faces are compared at fixed momentum scale. The body is the plain four-term sum; no lemmas.
Claim. For a real wave covector $k \in \mathbb{R}^4$, define $\|k\|^2 := \sum_{i=0}^{3} k_i^2$.
background
The module freezes the independent continuum target for the 4D Regge weak-field campaign before any recovery proof: canonical periodic Freudenthal 4-torus of side $N \ge 3$, Frobenius-normalized Euclidean TT polarizations, and an Einstein-Hilbert quadratic fixed by kappa_einstein rather than lattice fitting. Continuum Tendsto Props remain open; nothing here claims EH recovery.
A wave covector is an element of Wave4, the type of maps $\mathrm{Fin},4 \to \mathbb{R}$, i.e. a real 4-tuple of Bloch/momentum components on the torus. The same squared-norm definition appears upstream in the exact midpoint $m^2$ TT identity module; the preflight copy is definitionally identical and is re-exported so continuum bookkeeping stays local to this file.
Downstream, $|k|^2$ normalizes exact flat cross-term symbols, separates banked $m^2$ coefficients from geometric certificate values at fixed direction, and appears in the packaged edge TT decomposition (nonzero-momentum hypothesis).
proof idea
Pure definition: expand the squared Euclidean norm as the sum of four products $k_i \cdot k_i$ over $\mathrm{Fin},4$. No tactics, no lemmas. Sibling equality waveNormSq_eq_momentumSq and the private bridge waveNormSq_preflight_eq_identity later identify this with the upstream identity-module copy by rfl.
why it matters
Local scale for every continuum-facing symbol comparison in the 4D Regge preflight. Downstream, waveId_symbolDir evaluates it at the fixed direction symbolDir to get 2, which feeds banked_coefficient_is_not_the_certificate_value (normalization mismatch between per-unit-momentum $m^2$ coeffs and geometric certificates). The Recognition-mesh exact-$J$ bridge uses the preflight/identity equality when closing EH and pure-gauge faces. The packaged OPEN edge TT decomposition requires waveNormSq m ≠ 0 before splitting Hessian data into TT, gauge, and residual-trace parts.
In the broader QG campaign this is scaffolding for the frozen EH target and honesty decoys: continuum recovery (S_RS_converges_EH_4d, gap action) stays uninhabited; the norm only supplies the $|k|^2$ denominator the later algebraic closer must observe, never fit. Ties to the D=3 spatial plus time lattice setting of the eight-tick / 4D mesh story without claiming continuum limit theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.