axisTTPlusNormalized
plain-language theorem explainer
Defines the Frobenius-normalized axis plus TT polarization in 4D Euclidean signature: the matrix diag(0,0,1,−1) scaled by 1/√2 so that its Frobenius norm is 1. Gravity analysts cite it as the canonical plus-mode witness for continuum EH-target hypotheses and TT nonvacuity. The body is a one-line scalar multiple of the unnormalized axis plus matrix.
Claim. Let $H_+ = \mathrm{diag}(0,0,1,-1)$ be the unnormalized axis plus polarization in $\mathrm{Mat}_4(\mathbb{R})$. Define the normalized plus polarization $H_+^{\mathrm{n}} := \frac{1}{\sqrt{2}}\, H_+$, so that $\|H_+^{\mathrm{n}}\|_F = 1$.
background
This module freezes continuum preflight data for the 4D Regge-to-Einstein–Hilbert campaign: canonical Freudenthal 4-torus mesh, Frobenius-normalized Euclidean TT polarizations, an independently fixed linearized EH quadratic, and named OPEN continuum targets. Nothing here proves continuum recovery; it only locks the contracts before further computation.
Mat4 is the type of real $4\times 4$ matrices. The upstream object axisTTPlus is the unnormalized plus polarization with only nonzero entries $H_{22}=1$ and $H_{33}=-1$ (i.e. $\mathrm{diag}(0,0,1,-1)$). Frobenius normalization to unit norm is the Gate A0 analog required by the frozen TT contracts: continuum symbol comparisons and EH coefficient checks are stated on unit-Frobenius TT data so scale is not free.
The plus mode pairs with a cross polarization; both serve as concrete witnesses that the TT hypothesis class used by continuum targets is nonempty.
proof idea
Pure definition: scalar multiplication of the unnormalized axis plus matrix by the reciprocal of $\sqrt{2}$. No tactics or lemmas. The factor $1/\sqrt{2}$ is the unique positive constant that makes the Frobenius norm of $\mathrm{diag}(0,0,1,-1)$ equal to 1, since that matrix has two $\pm 1$ diagonal entries and Frobenius squared norm $1^2+(-1)^2=2$.
why it matters
This is the frozen normalized plus witness for the Regge 4D continuum preflight. Downstream it feeds axisTTPlusNormalized_isTT and axisTTPlusNormalized_isTTPolarization (proving it is transverse-traceless with unit Frobenius norm), and through those continuum_target_hypothesis_nonvacuous and the algebraic closer's tt_witnesses_nonvacuous and plus_normalized_isTTPolarization.
It also appears in the OPEN agreement target Regge4DPlusCrossAgreeTarget: continuum symbols on the axis mode for plus and cross normalized polarizations must yield the same coefficient. The module's binding contracts require Frobenius-normalized Euclidean TT data before any Tendsto or EH-recovery claim; this definition discharges that contract for the plus channel without reverse-engineering lattice weights from the EH answer.
In the broader QG campaign it is scaffolding for later continuum closure (still OPEN: S_RS_converges_EH_4d uninhabited; gap action recovery false), not a physics derivation of $D=3$ or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.