star_flat_angle_sum_two_pi
plain-language theorem explainer
Around the seed triangle hinge in the full 4D Freudenthal lattice star, the sum of the six flat dihedral angles equals exactly 2π. Lattice-Regge and recognition-mesh workers cite this as the flatness gate before any deficit class is assigned. The proof substitutes the four opposite angles π/4 and two orthogonal angles π/2, then finishes by ring arithmetic.
Claim. The star flat-angle sum around the seed hinge equals $2\pi$. Explicitly, with four opposite flat angles each equal to $\pi/4$ and two orthogonal flat angles each equal to $\pi/2$, one has $4\cdot(\pi/4)+2\cdot(\pi/2)=2\pi$.
background
This module is the next kernel-checked increment in the 4D Regge campaign after the dihedral cosine kernel. It treats the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star: four containing unit cubes and six incident 4-simplices on the integer lattice. Other hinge orbits remain open.
Flat angles are the dihedral angles of those simplices in the Euclidean (zero-curvature) embedding, read from each orbit's Gram vector. Four simplices carry opposite-type flat cosine $1/\sqrt{2}$, hence angle $\pi/4$; two carry orthogonal-type flat cosine $0$, hence angle $\pi/2$. The star sum is defined as four times the opposite angle plus twice the orthogonal angle.
Upstream equalities already pin those two angles: the opposite angle is $\arccos(1/\sqrt{2})=\pi/4$ and the orthogonal angle is $\arccos(0)=\pi/2$. The present statement is the flatness gate that those values sum to a full turn.
proof idea
Term-mode, three lines. Unfold the definition of the star sum together with the two upstream angle identities (opposite equals $\pi/4$, orthogonal equals $\pi/2$). The resulting rational multiple of $\pi$ is then reduced by ring to $2\pi$. No case splits, no analysis beyond the already-proved arccos evaluations.
why it matters
Deliverable A.3 of the module: the flatness gate on the full star. Downstream it is handed to the closed typed residuals that identify the mesh geometric deficit (R1) and the hinge kappa (R2); both refine packages list this equality among their witnesses. Sibling star-kernel modules for other hinge types reuse the same pattern, so the seed case anchors the family.
In the broader Recognition gravity stack this is a local Euclidean consistency check on the 4D lattice before deficit classes $(2,3,6,7,10,11,14)$ are assigned values $(-1,-1,+1,-1,+1,+1,-1)$. It does not yet assemble the flat Hessian over all hinges, nor does it touch action recovery or the continuum Einstein–Hilbert limit; those remain explicitly open in the module tier tags.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.