flatAngleSeedOpp_eq
plain-language theorem explainer
The opposite-orbit flat seed angle around the Regge seed hinge equals π/4. Lattice-gravity and discrete-curvature workers cite it when converting the Gram cosine 1/√2 into a concrete angle for the six-simplex star. The proof is a one-line wrapper of the classical arccos identity arccos(1/√2)=π/4.
Claim. The flat seed angle for the opposite-edge orbit equals $\pi/4$: if that angle is defined by $\arccos(1/\sqrt{2})$, then it equals $\pi/4$.
background
In 4D Regge calculus on the integer lattice, curvature is carried by hinge deficits: the failure of dihedral (or face) angles around a triangle to sum to $2\pi$. This 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 angles are read from each simplex's Gram data. The opposite-orbit cosine is $1/\sqrt{2}$, so the corresponding seed angle is defined as $\arccos(1/\sqrt{2})$. A companion orthogonal-orbit angle uses cosine $0$. The module's deliverable is the flat cosine multiset and the flatness gate that the star angle sum is exactly $2\pi$.
Upstream, the identity $\arccos(1/\sqrt{2})=\pi/4$ is already proved by matching $\cos(\pi/4)=\sqrt{2}/2$ with the algebraic rewrite $1/\sqrt{2}=\sqrt{2}/2$.
proof idea
One-line wrapper: the claim is definitionally the statement of the upstream identity $\arccos(1/\sqrt{2})=\pi/4$, so the proof simply applies that theorem. No extra algebra is done here.
why it matters
Parent use is the flatness gate: the star angle sum equals $2\pi$. That proof unfolds the sum, rewrites both seed angles via this identity and its orthogonal twin, then closes by ring. Without collapsing the opposite seed to $\pi/4$, the six-angle sum cannot simplify.
In the module's deliverable list this is a brick under items 2–3 (flat cosine multiset and flatness gate) of the QG full-theory campaign kernel after the dihedral kernel. It does not finish Hessian assembly, action convergence $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery; those remain open. Scope is the seed hinge orbit only.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.