waveNormSq_axisWave
plain-language theorem explainer
The squared Euclidean norm of the standard axis wave covector (1,0,0,0) equals 1. Downstream discrimination lemmas cite it to pin the witness product ‖H‖²_F · |k|² away from zero and to evaluate the exact midpoint Bloch second variation at −1/4. The proof is a one-line numerical reduction of the four-term sum.
Claim. If $k = (1,0,0,0) \in \mathbb{R}^4$ is the axis wave covector, then its squared Euclidean norm satisfies $\sum_{i=0}^{3} k_i^2 = 1$.
background
This module sits in Arc 2, step 7 of the 4D Regge–continuum comparison. ContinuumTTSecondVariation4D already shows that the phase-averaged second variation of $\int R\sqrt{g}$ on a real transverse-traceless cosine wave is $-(1/4),|k|^2,|H|_F^2$. The present file leaves Regge's normalization $\rho$ free in $\sum_h A_h\delta_h = \rho\int R\sqrt{g}$ and forces $\rho=1/2$ by dictionary comparison.
The wave covector $k$ is a map $\mathrm{Fin},4\to\mathbb{R}$. Its squared Euclidean norm is the plain sum $\sum_i k_i^2$. The axis wave is the unit covector along the 0-direction: $k=(1,0,0,0)$. It is the standard probe used with the axis TT-plus polarization in the discrimination lemmas that pin $\rho$.
proof idea
One-line wrapper. Unfold the definitions of the squared wave norm and of the axis wave, expand the sum over $\mathrm{Fin},4$, and discharge $1^2+0^2+0^2+0^2=1$ by norm_num.
why it matters
The lemma is bookkeeping that makes the witness nondegenerate. It is rewritten into witness_nonzero (product of Frobenius and wave norms is nonzero), into dictionary_witness_value (exact midpoint Bloch second variation equals $-1/4$ on the axis pair), and into rho_one_fails (the $\rho=1$ face disagrees with the continuum value at that witness).
Those three results are the discrimination steps that separate Regge's action from $\int R\sqrt{g}$ and force $\rho=1/2$ (equivalently discreteBookkeepingFactor := 2). Without a unit wave norm the numerical comparison would be indeterminate. The result is pure 4D Euclidean linear algebra; it does not itself invoke the Recognition forcing chain, but it closes the classical-input gate A4 that the gravity side of the monolith needs before continuum and discrete faces can be identified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.