sqrt_two_mul_self
plain-language theorem explainer
Records the elementary identity $\sqrt{2}\cdot\sqrt{2}=2$. Gravity analysts in the Regge TT symbol preflight cite it when normalizing axis-wave polarizations and inverse-square-root edge weights. The proof is a one-line wrapper of the standard real-analysis fact that a nonnegative square root multiplies to its radicand.
Claim. The product of the positive square root of $2$ with itself equals $2$: $\sqrt{2}\cdot\sqrt{2}=2$.
background
The ambient module builds the true nonlinear 3D Regge action on the periodic Freudenthal torus and the TT Bloch symbol object used in the QG full-theory campaign (Stage 1). Edge lengths enter through square roots, and conformal or axis-aligned trial fields routinely produce factors of $\sqrt{2}$ from face diagonals and cubic lattice geometry.
Mathlib supplies Real.mul_self_sqrt: for any nonnegative real $x$, $\sqrt{x}\cdot\sqrt{x}=x$. Here the radicand is the constant $2$, whose nonnegativity is immediate. The sibling theorem inv_sqrt_two_sq rewrites $(1/\sqrt{2})^2=1/2$ by reducing to this identity, which is the form needed for TT polarization witnesses on axis wave vectors.
proof idea
One-line wrapper: apply Real.mul_self_sqrt to the constant $2$, discharging the nonnegativity side condition by norm_num. No further algebraic rearrangement is required.
why it matters
Feeds the immediate downstream identity inv_sqrt_two_sq, which states $(1/\sqrt{2})\cdot(1/\sqrt{2})=1/2$ and is annotated as supporting the $+$-witness TT polarization for axis wave vectors. That polarization sits inside the Regge TT continuum-symbol preflight: true nonlinear Regge action, flat-point checks, and the still-open continuum isotropy target ReggeTTContinuumIsotropyTarget (numerical evidence only; status flag false). The lemma itself is pure real arithmetic scaffolding, not a gravity claim, but without it the inverse-sqrt normalizations in the TT symbol object do not type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.