sqrt_half
plain-language theorem explainer
The elementary identity $\sqrt{1/2}=\sqrt{2}/2$ on the reals. Cited by the four flat-hinge area evaluations that reduce Heron squares to $1/2$ on the Freudenthal 4-simplex seed. Proof rewrites $1/2$ as $(\sqrt{2}/2)^2$ and applies the square-root-of-square lemma.
Claim. On the reals, $\sqrt{1/2} = \sqrt{2}/2$.
background
The module develops a pathwise Schläfli identity for the Freudenthal (Kuhn) 4-simplex at $n_H=n_E=10$, mirroring the 3D Gate-A2 tetrahedron input. Flat hinge areas are computed from squared edge lengths via Heron's formula; several seed hinges produce the intermediate square $1/2$.
hingeAreaFlat evaluates the area of a triangle hinge on the flat seed by feeding three squared edge lengths into Heron and taking a square root. Sibling lemmas already reduce those Heron squares to the constant $1/2$ by direct arithmetic on the seed edge table.
This lemma is the final algebraic cleanup that converts $\sqrt{1/2}$ into the conventional form $\sqrt{2}/2$ used in the flat Schläfli summand table.
proof idea
Term-mode rewrite. First establish the intermediate equality $1/2=(\sqrt{2}/2)^2$ by expanding the square via div_pow and Real.sq_sqrt (nonnegativity of 2 by norm_num), then simplify the arithmetic. With that identity in hand, apply Real.sqrt_sq under a positivity side-goal to conclude $\sqrt{1/2}=\sqrt{2}/2$.
why it matters
Feeds the four concrete flat-area theorems hingeAreaFlat_1, hingeAreaFlat_3, hingeAreaFlat_7, and hingeAreaFlat_8, each of which ends by rewriting through this identity after a Heron-square evaluation. Those areas populate the flat Schläfli summand table that witnesses a non-vacuous SchlaefliIdentityN at $n_H=n_E=10$ with strictly positive areas (module THEOREM tier).
The table is Gate-A2-style input for the flat directional Schläfli kill along every affine velocity through the seed. It does not close the OPEN pathwise identity off the flat seed, nor the elevation to the continuum Einstein-Hilbert candidate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.