inv_sqrt2_mul_self
plain-language theorem explainer
Algebraic identity: the product of two factors of one over square root of two equals one half. Cited wherever the Frobenius-normalized TT witness polarization E = diag(1,-1,0)/√2 is expanded in the Regge hinge-aware zero-mode gate. Proof is a one-line rewrite chaining division commutation with the companion fact √2·√2 = 2.
Claim. One has $\bigl(1/\sqrt{2}\bigr)\cdot\bigl(1/\sqrt{2}\bigr) = 1/2$ as a real equality.
background
This module closes Gate C-A3 of the QG full-theory campaign (Paper C / Pillar 1): the hinge-aware zero mode of the assembled Regge TT constant block. The reported TT witness is the polarization $E = \mathrm{diag}(1,-1,0)/\sqrt{2}$ with wave vector $k = e_z$. Frobenius normalization of that matrix forces factors of $1/\sqrt{2}$ into every edge-class coefficient and every residual evaluation.
The companion local fact sqrt2_mul_self already records $\sqrt{2}\cdot\sqrt{2} = 2$ (via Real.mul_self_sqrt). The present identity is the reciprocal form needed when those factors appear as denominators rather than numerators. Upstream arithmetic lemmas supply the unit-multiplication rewrite used in the chain.
proof idea
One-line wrapper. Rewrite with div_mul_div_comm to obtain $(1\cdot 1)/(\sqrt{2}\cdot\sqrt{2})$, collapse the numerator by one_mul, then apply the local companion sqrt2_mul_self to replace the denominator by 2, yielding $1/2$.
why it matters
Feeds two immediate parents in the same module. First, inv_sqrt2_sq lifts the product identity to the squared form $(1/\sqrt{2})^2 = 1/2$, the natural shape for Frobenius norms. Second, ttWitness_isTT uses the normalized coefficients to prove the reported witness really is a TT polarization for $k = e_z$: symmetric, traceless, transverse, and Frobenius-normalized. That theorem grounds the phrase "the reported TT witness" attached to the kernel-recorded residual, and thereby underwrites the headline zero-mode cancellation assembledConstantBlock_eq_zero and the assembly-sign pin assembled_witness_split. Without the reciprocal square-root arithmetic, the normalization half of the TT check does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.