flatAngleSeedOpp
plain-language theorem explainer
Names the flat dihedral angle for the opposite-orbit simplices in the seed hinge star: arccos(1/√2). Downstream star-sum and flatness-gate arguments cite it as the four-fold contribution. The body is a pure real constant; equality to π/4 is a separate one-line lemma.
Claim. The opposite-orbit flat seed angle is the real number $\arccos(1/\sqrt{2})$.
background
In the Regge 4D star-kernel module, the seed triangle hinge ${0,e_0,e_0+e_1}$ sits in a full periodic Freudenthal star: four unit cubes and six incident 4-simplices. Flat dihedral cosines on those simplices split into two orbits: four simplices carry cosine $1/\sqrt{2}$ and two carry cosine $0$, each read from the orbit's Gram vector.
This constant packages the arccos of the opposite-orbit cosine. The orthogonal-orbit companion is the analogous arccos of $0$. Their linear combination is the star flat-angle sum used to gate exact flatness (sum $=2\pi$) before any deficit-class kernel is assembled.
The module never redefines the dihedral-cosine or stencil APIs; it only enumerates the star and evaluates these seed angles.
proof idea
Pure definition: the real constant $\arccos(1/\sqrt{2})$. No proof body. The companion theorem flatAngleSeedOpp_eq discharges the identity with $\pi/4$ via the standard arccos lemma for $1/\sqrt{2}$.
why it matters
Supplies the four-fold term in the star flat-angle sum $4\cdot\mathrm{flatAngleSeedOpp}+2\cdot\mathrm{flatAngleOrth}$. That sum is the flatness gate (deliverable A.3) of the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$. Without a named opposite seed angle, the multiset of flat cosines cannot be turned into an exact $2\pi$ identity. The module still leaves other hinge orbits, full Hessian assembly, and $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.