star_flat_angle_sum_two_pi
plain-language theorem explainer
For a type-(1,3) Regge triangle hinge on the 4D periodic lattice, the sum of the six flat dihedral angles in its Freudenthal star equals exactly 2π. Residual-closure and flatness-gate arguments in the Recognition mesh geometric-deficit layer cite this identity. The proof is a one-line reduction: unfold six times the common flat angle and substitute arccos(1/2)=π/3.
Claim. The flat angle sum over the full Freudenthal star of a type-$(1,3)$ triangle hinge equals $2\pi$. Concretely, each of the six Kuhn simplices has flat angle $\arccos(1/2)=\pi/3$, so $6\cdot(\pi/3)=2\pi$.
background
In the 4D Regge hinge analysis for Recognition gravity, hinges are stratified by Freudenthal orbit type. The type-$(1,3)$ triangle hinge uses absolute masks ${0,e_0,e_0+e_1+e_2+e_3}$ (difference masks $(1,14)$) with local flat squared lengths $(1,3,4)$. Exactly six Kuhn simplices in the origin unit cube contain the hinge; among cube translates in ${-1,0,1}^4$ only the origin does.
All six simplices share the same Gram vector of local squared lengths, hence the same flat cosine $1/2$ and flat angle $\arccos(1/2)$. The star flat angle sum is defined as six times that common angle. The module is the kernel-checked increment after the type-$(1,1)$ seed orbit; it imports the Freudenthal incidence layer, the 15-class stencil, and the Gram-projection cosine calculus without redefining their API.
Upstream, the type-$(1,3)$ flat angle is already identified with $\pi/3$ via the standard arccos-of-one-half lemma.
proof idea
One-line term proof. Unfold the definition of the star flat angle sum (six copies of the type-$(1,3)$ flat angle) and rewrite by the already-proved identity that this flat angle equals $\pi/3$. The resulting scalar $6\cdot(\pi/3)$ is reduced by ring arithmetic to $2\pi$. No star enumeration or cosine recomputation occurs in this step; those live in the supporting lemmas that supply the angle identity.
why it matters
This is deliverable A.3 of the type-$(1,3)$ kernel: the flatness gate (star angle sum exactly $2\pi$). Downstream it is a required witness in the closed typed residuals for mesh geometric deficit (R1) and hinge kappa (R2), and it sets the flatnessGateClosed flag in the kernel status record.
In the QG full-theory campaign the result is the discrete flat-space condition (vanishing deficit) for one orbit class in the 15-class stencil, needed before curvature can be matched to the Einstein-Hilbert side. Complementary type-$(3,1)$ transport, full flat Hessian assembly over all hinges, $S_{\mathrm{RS}}\to\mathrm{EH}$ convergence, and gap-action recovery remain explicitly open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.