flatAngleOrth_eq

In 4D Regge calculus on the integer lattice, curvature lives on triangular hinges. The module treats the seed hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star: four unit cubes, six incident 4-simplices. Flat dihedral angles are read from each simplex's Gram vector; the multiset splits into four angles with cosine $1/\sqrt{2}$ and two with cosine $0$.

The orthogonal class is the cosine-$0$ orbit. Its angle is defined as $\arccos(0)$. The companion opposite-class angle is handled by a parallel identity. Together they feed the flatness gate: the star angle sum must equal exactly $2\pi$ before any deficit class kernel is written down.

Scope is deliberately local. Other hinge orbits of the lattice remain open; this kernel does not assemble the full flat Hessian or claim Einstein–Hilbert recovery.

One-line wrapper. The definition sets the orthogonal flat angle to $\arccos(0)$; the theorem rewrites it by the Mathlib lemma Real.arccos_zero, which states $\arccos(0)=\pi/2$. No lattice combinatorics or Gram-determinant work is needed at this step.

This identity is the orthogonal half of the flatness gate. Downstream, star_flat_angle_sum_two_pi substitutes both the opposite-class and orthogonal-class equalities and closes by ring arithmetic to obtain star angle sum $=2\pi$. That gate is deliverable A.3 of the module: without exact flatness, the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$ has no geometric meaning.

In the QG campaign this is the next kernel-checked increment after the two-simplex dihedral cosine calculus. It does not yet flip gap-action recovery or prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D; it only locks the flat reference configuration for the seed hinge orbit.