axisTTCrossNormalized
plain-language theorem explainer
The Euclidean axis cross TT polarization, scaled by 1/√2 so its Frobenius norm equals one. Gravity analysts cite it as the normalized cross witness when freezing continuum Einstein-Hilbert targets on the 4-torus mesh. The body is a one-line scalar multiple of the unnormalized cross matrix with H₂₃ = H₃₂ = 1.
Claim. Define the Frobenius-normalized axis cross polarization as the $4\times 4$ real matrix $H^{\times}_{\mathrm{norm}} = \frac{1}{\sqrt{2}}\, H^{\times}$, where the unnormalized cross matrix $H^{\times}$ has entries $H^{\times}_{23} = H^{\times}_{32} = 1$ and zeros elsewhere. The factor $1/\sqrt{2}$ makes the Frobenius norm equal to $1$.
background
This module freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation. Nothing here proves continuum recovery. The carrier is the periodic Freudenthal 4-torus of side $N\ge 3$; continuum targets quantify over Frobenius-normalized Euclidean TT polarizations (Gate A0 analog).
A Mat4 is a $4\times 4$ real matrix. Upstream, the unnormalized axis cross polarization places $1$ in the $(2,3)$ and $(3,2)$ slots and zeros elsewhere: the standard Euclidean TT cross mode on the spatial axes. Its Frobenius squared norm is $2$ (two unit off-diagonal entries), so dividing by $\sqrt{2}$ pins the norm to one.
The EH quadratic is frozen independently via kappa_einstein; later algebraic closers must observe equality on these normalized witnesses, never fit a lattice scale.
proof idea
One-line definition: left-scalar-multiply the unnormalized axis cross matrix by $(\sqrt{2})^{-1}$. No lemmas are invoked; the scale is the reciprocal square root of the unnormalized Frobenius squared norm (two unit entries).
why it matters
Supplies the normalized cross witness required by the frozen continuum contracts. In-module parents prove it is TT and a TT polarization (paired with the Frobenius-norm-squared pin), and that the OPEN continuum target quantifies over a nonempty TT class (plus and cross witnesses).
The algebraic closer re-exports those facts and uses this matrix in the OPEN plus-cross agreement target: continuum symbols on the axis mode for plus and cross normalized polarizations must agree. That target is part of the QG full-theory campaign's first binding increment toward 4D continuum closure. Banked algebraic faces and discrete bookkeeping remain separate from geometric Tendsto Props; continuum recovery (S_RS_converges_EH_4d) stays uninhabited.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.