flatAngleT13
plain-language theorem explainer
Names the common flat interior angle of the six Kuhn simplices around a type-(1,3) triangle hinge as arccos(1/2). Gravity analysts cite it when assembling the periodic Freudenthal star deficit and the flatness gate. The body is a one-line real constant definition.
Claim. The flat angle for the type-$(1,3)$ hinge is defined by $\theta_{13}^{\mathrm{flat}} := \arccos(1/2)$.
background
This module builds the Regge 4D type-(1,3) star deficit kernel on the periodic Freudenthal lattice. The hinge is the triangle with absolute masks ${0, e_0, e_0+e_1+e_2+e_3}={0,1,15}$, local flat squared lengths $(1,3,4)$, and difference masks $(1,14)$. Exactly six Kuhn simplices in the origin unit cube contain the hinge; cube translates in ${-1,0,1}^4$ contribute only at the origin.
Flat geometry on each simplex is read from the Gram-projection cosine calculus already fixed in the imported dihedral and flat kernels. For this length triple the shared flat cosine is $1/2$, so every simplex contributes the same interior angle $\arccos(1/2)$. The star angle sum is then six copies of that value; flatness requires the sum equal $2\pi$.
proof idea
Pure definition: bind the real constant Real.arccos (1/2). No lemmas, no tactics. Downstream equality to $\pi/3$ is proved separately by the standard identity arccos_one_half.
why it matters
Supplies the atomic flat angle used by flatAngleT13_eq (proves the value is $\pi/3$) and by starFlatAngleSum (six-fold multiple). Together they discharge deliverable A.3 of the module: the star angle sum equals exactly $2\pi$, the flatness gate for the type-(1,3) full-star deficit class kernel on classes $(1,3,5,7,9,11,13)$. That kernel is the next checked increment after the type-(1,1) seed orbit; it does not yet finish Hessian assembly, $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, or gap-action recovery, and transport to the complementary type $(3,1)$ remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.