inv_sqrt_two_sq
plain-language theorem explainer
The elementary identity $(1/\sqrt{2})\cdot(1/\sqrt{2})=1/2$. Gravity analysts cite it when unit-normalizing the axis plus and cross TT polarization tensors under the Frobenius norm. The proof is a three-step rewrite: commute the divisions, cancel $1\cdot 1$, then apply $\sqrt{2}\cdot\sqrt{2}=2$.
Claim. One has $\bigl(1/\sqrt{2}\bigr)\cdot\bigl(1/\sqrt{2}\bigr)=1/2$ as an equality of real numbers.
background
This module is Stage 1 of the Regge TT continuum-symbol campaign: it builds the true nonlinear 3D Regge action on the periodic Freudenthal torus as a function of an arbitrary edge squared-length field, freezes the flat background, and packages the TT Bloch symbol object for later continuum analysis.
Axis TT polarizations (the $+$ and $\times$ witnesses for a coordinate-axis wave vector) are scaled by $1/\sqrt{2}$ so that their Frobenius norms become one. The same scalar appears in the 4D continuum preflight when those normalized tensors are fed into Frobenius-norm-squared identities.
The local lemma $\sqrt{2}\cdot\sqrt{2}=2$ (sibling sqrt_two_mul_self) is the only non-library arithmetic input; everything else is ordinary field algebra on $\mathbb{R}$.
proof idea
Three rewrites, no case splits. First div_mul_div_comm turns the product of quotients into a single quotient of products. Then one_mul collapses the numerator $1\cdot 1$. Finally the sibling identity $\sqrt{2}\cdot\sqrt{2}=2$ rewrites the denominator, leaving $1/2$.
why it matters
Unit Frobenius norm of the normalized axis $+$ and $\times$ TT tensors is proved downstream by scaling the un-normalized norms with this identity (frobeniusNormSq_axisTTPlusNormalized, frobeniusNormSq_axisTTCrossNormalized in the 4D continuum preflight, and the local TT-polarization certificates axisTTPolarizationPlus_isTT, axisTTPolarizationCross_isTT).
Those certificates sit inside the ReggeTTContinuumSymbol program: they supply the discrete TT projectors whose Bloch symbol is later compared to the Einstein-Hilbert coefficient $-1/4$. The continuum isotropy target itself remains open (status flag false); this lemma only clears the algebraic bookkeeping that makes the normalized witnesses well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.