sqrt_three_quarter
plain-language theorem explainer
Algebraic identity $\sqrt{3/4}=\sqrt{3}/2$ on the reals. Cited by the flat-hinge area evaluations that feed the 4-simplex Schläfli summand table at the Freudenthal seed. Proof is a two-step rewrite: square the right-hand side, then apply $\sqrt{\,\cdot\,}^2$.
Claim. On the reals, $\sqrt{3/4} = \sqrt{3}/2$.
background
The ambient module develops the pathwise Schläfli identity for the Freudenthal (Kuhn) 4-simplex at $n_H=n_E=10$, mirroring the 3D Gate-A2 closed form for the tetrahedron. Flat hinge areas are computed from squared edge lengths via Heron's formula: after reducing the three boundary edge-squares of a hinge, one obtains a radicand that is often $3/4$ at the flat seed.
Sibling lemmas already record $\sqrt{1/4}=1/2$ and $\sqrt{1/2}$. The present identity is the remaining elementary radical needed when Heron's squared area evaluates to $3/4$. Downstream, two of the ten flat hinge areas equal $\sqrt{3}/2$ exactly because of this reduction.
No Recognition-Science forcing step (T5–T8) is invoked; the lemma is pure real arithmetic supporting the geometric kernel.
proof idea
Term-mode rewrite. First establish the algebraic identity $3/4=(\sqrt{3}/2)^2$ by expanding the square via div_pow and cancelling $\sqrt{3}^2=3$ (nonnegativity of 3 by norm_num). Then apply Real.sqrt_sq with a positivity side-goal, which yields $\sqrt{(\sqrt{3}/2)^2}=\sqrt{3}/2$.
why it matters
Closes the radical step in hingeAreaFlat_2 and hingeAreaFlat_5, both of which assert that the corresponding flat hinge areas equal $\sqrt{3}/2$. Those values populate the flat Schläfli summand table (THEOREM tier in the module doc): column sums vanish and the seed-hinge row matches hingeArea · angleKernel from the 4D dihedral kernel.
The table is the Gate-A2-style input for the flat directional Schläfli kill along every affine velocity through the seed. It does not touch the still-open pathwise identity off the flat seed, nor S_RS_converges_EH_4d, nor gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.