flatAngleRight_eq
plain-language theorem explainer
Identifies the right dihedral angle used for the type-(1,2) flat star as exactly π/2. Anyone assembling the four-simplex flatness gate for the Regge (1,2) hinge cites this equality. The proof is a one-line appeal to the standard identity arccos(0)=π/2.
Claim. The flat right dihedral angle, defined as $\arccos 0$, equals $\pi/2$.
background
This module builds the full periodic-lattice star deficit kernel for the Regge 4D type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$). The campaign enumerates the four incident Kuhn 4-simplices in the integer lattice and checks that each carries flat cosine $0$, so the star angle sum is exactly $2\pi$.
The local constant flatAngleRight is defined as $\arccos 0$. It is the common flat dihedral angle assigned to every simplex in that star once the Gram-projection cosine calculus has returned cosine zero on both squared-length orbits. The identity proved here converts that cosine into an explicit radian measure needed for the angle-sum gate.
proof idea
One-line wrapper: the goal is definitionally $\arccos 0 = \pi/2$, which is exactly the Mathlib lemma Real.arccos_zero. No further rewriting or case analysis is required.
why it matters
Feeds directly into star_flat_angle_sum_two_pi, which rewrites the four-fold star sum as $4\cdot(\pi/2)=2\pi$ and thereby discharges the flatness gate for the type-(1,2) orbit. That gate is deliverable A.3 of the module: without the exact $\pi/2$ value the star deficit class kernel (values $\pm\sqrt{2}/2$ on the 15 stencil classes) cannot be certified as a pure curvature defect on a flat background.
In the broader QG campaign this is a kernel-checked increment after the type-(1,1) seed orbit; the complement type-(2,1) and the remaining hinge orbits stay open, and the result does not yet assemble the full flat Hessian or flip gap_action_recovery / S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.