m2TransportedAllOrbitMomentDistinctHinge_axisTTCrossNormalized_e0Dir
plain-language theorem explainer
The distinct-hinge all-orbit m² moment of the unit-normalized TT cross polarization on the bare lattice axis e₀ equals −1/16. Gravity analysts cite it when matching continuum face values on axis modes. The proof scales the unnormalized cross certificate (−1/8) by (√2)⁻² via the smul lemma and simplifies.
Claim. Let $H^\times$ be the unnormalized TT cross polarization ($H_{23}=H_{32}=1$) and let $\hat H^\times=(\sqrt{2})^{-1}H^\times$. On the axis ray $e_0=(1,0,0,0)$, the transported all-orbit distinct-hinge moment equals $-1/16$.
background
This module certifies transported all-orbit $m^2$ evaluations for Regge–Bloch modes in 4D. The distinct-hinge moment folds orbit contributions with weights $1/r_\tau$, refining the raw all-orbit sum. Module context already closes plus and cross on the isotropic symbol direction (both distinct-hinge $-1/4$), and records that normalized plus/cross give raw $-1/8$ there.
The cross witness $H^\times$ is the symmetric off-diagonal matrix with only $H_{23}=H_{32}=1$. The factor $(\sqrt{2})^{-1}$ unit-normalizes that Frobenius mass. The probe direction $e_0$ is the bare lattice axis $(1,0,0,0)$, not the continuum symbol ray. Upstream, the unnormalized evaluation on this pair is already known: distinct-hinge of bare cross on $e_0$ is $-1/8$, and the moment is homogeneous of degree two under scalar multiplication of the polarization.
proof idea
Term-mode rewrite chain. First apply the scalar-homogeneity lemma for the distinct-hinge moment, pulling $(\sqrt{2})^{-1}$ out as $(\sqrt{2})^{-2}$ times the unnormalized value. Substitute the bare-cross certificate on $e_0$, which equals $-1/8$. Reduce $(\sqrt{2})^{-2}$ via inv_pow and Real.sq_sqrt (using $2\ge 0$), then finish by norm_num to $-1/16$.
why it matters
Feeds the algebraic closer continuumFace_normalizedCross_e0Dir, which states that on $e_0$ the normalized cross already hits the continuum face value $-1/16$ (since $|e_0|^2=1$), while normalized plus hits $0$. That mismatch is the explicit witness that continuum TT isotropy fails on the bare axis mode: the module flags Regge4DContinuumIsotropyBlockedOnAxisMode as open/false, and notes that the full cosine two-jet does not repair $e_0$ anisotropy or plus vanishing.
In the gravity analysis stack this is a lattice-mode certificate, not a continuum recovery step. It does not flip gap_action_recovery. It sits downstream of the transported-orbit machinery and upstream of face-normalization bookkeeping used when comparing Regge discrete spectra to continuum TT projectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.