flatAngleOrth
plain-language theorem explainer
Names the flat dihedral angle for the orthogonal Gram orbit as arccos(0). In the seed-hinge star, two of the six incident 4-simplices carry flat cosine 0; this constant is that angle. Downstream proofs identify it with π/2 and fold two copies into the star angle sum that gates flatness at 2π.
Claim. The orthogonal flat angle is defined by $\mathrm{flatAngleOrth} := \arccos(0) \in \mathbb{R}$.
background
This module builds the full periodic Freudenthal star of the seed triangle hinge ${0,e_0,e_0+e_1}$ in the integer lattice: four containing unit cubes and six incident 4-simplices. It sits one kernel increment past the two-simplex dihedral cosine calculus and the 15-class edge stencil.
Flat geometry on each simplex is read from its own Gram vector. The star's flat-cosine multiset splits into two orbits: four simplices with cosine $1/\sqrt{2}$ and two with cosine $0$. The present definition isolates the angle belonging to the cosine-$0$ orbit.
The star flatness gate requires the sum of the six flat dihedral angles to equal exactly $2\pi$. That sum is assembled as four copies of the opposite-orbit angle plus two copies of this orthogonal angle.
proof idea
Pure definition: bind the real constant to Real.arccos 0. No lemmas, no tactics. The companion theorem flatAngleOrth_eq later rewrites it to $\pi/2$ via Real.arccos_zero.
why it matters
Supplies the orthogonal contribution to the star angle sum. starFlatAngleSum is defined as $4\cdot\mathrm{flatAngleSeedOpp}+2\cdot\mathrm{flatAngleOrth}$; the flatness gate (deliverable A.3) asserts that sum equals $2\pi$. That gate is a prerequisite for the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$.
In the QG campaign this is local scaffolding for Regge curvature on the lattice, not yet Einstein–Hilbert recovery: the module explicitly does not flip gap_action_recovery or prove $S_{\mathrm{RS}}$ converges to EH in 4D. Other hinge orbits remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.