flatAngleRight
plain-language theorem explainer
Names the flat dihedral angle for the type-(1,2) Regge hinge as arccos(0), i.e. a right angle. Downstream star-sum and flatness-gate lemmas cite it as the common angle of all four incident 4-simplices. The body is a one-line real constant, not a proof.
Claim. Define the flat right dihedral angle by $\mathrm{flatAngleRight} := \arccos(0) \in \mathbb{R}$.
background
This module builds the full periodic Freudenthal star for the type-(1,2) triangle hinge ${0, e_0, e_0+e_1+e_2}$ in the integer lattice (masks $0,1,7$). The campaign is a kernel-checked increment of 4D Regge calculus toward Recognition Science gravity: enumerate the star, recompute flat cosines from Gram data, and gate the angle sum to $2\pi$.
For this orbit the committed cosine calculus yields flat cosine $0$ on every incident 4-simplex (two local squared-length orbits). The corresponding dihedral angle is therefore a right angle. The constant packages that angle so the star sum and deficit-class kernel can refer to it by name rather than inlining $\arccos 0$.
The module imports the dihedral kernel, flat kernel, and 15-class edge stencil; it does not redefine their APIs.
proof idea
Pure definition: bind the real constant to $\mathrm{Real.arccos}, 0$. No tactics, no lemmas. The companion theorem flatAngleRight_eq later reduces it to $\pi/2$ via Real.arccos_zero.
why it matters
Delivers the common flat angle used by the type-(1,2) star flatness gate. starFlatAngleSum is defined as $4\cdot\mathrm{flatAngleRight}$, and the module claims that sum equals $2\pi$ (four right angles), which is deliverable A.3 of the kernel campaign.
That gate is a necessary checkpoint before the full-star deficit class kernel (values $\pm\sqrt{2}/2$ on the 15 stencil classes) and the nonvacuity, swap-symmetry, scaling-decoy, and homothety-stationarity gates. It does not yet assemble the flat Hessian over all hinge orbits, prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, or close gap_action_recovery. The complement orbit type (2,1) remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.