flatAngleT22
plain-language theorem explainer
Defines the flat dihedral angle of each simplex in the type-(2,2) Regge hinge star as arccos(0). Gravity analysts cite it when assembling the four-simplex flat angle sum that must equal 2π. It is a one-line real constant, later identified with π/2.
Claim. Let $\theta_{\mathrm{flat}}^{(2,2)} := \arccos(0) \in \mathbb{R}$. This is the common flat dihedral angle at the type-(2,2) triangle hinge in each of the four incident Freudenthal simplices.
background
The module treats the full periodic Freudenthal star of the type-(2,2) triangle hinge with vertex masks ${0,3,15}$ (difference masks $(3,12)$) inside the 4D axis-aligned unit-cube lattice. It sits one increment after the type-(1,1) seed-orbit kernel and reuses the Gram-projection cosine calculus rather than redefining it.
For each of the four star simplices the hinge-ordered flat squared-length vector is $(2,4,1,3,2,1,1,3,1,2)$. Direct evaluation of the projected Gram data yields cosine of the dihedral angle equal to $0$ on every incident simplex. The constant here packages that common angle as $\arccos(0)$ so the star sum can be written without repeating the inverse cosine.
The local deliverable is the flatness gate: four copies of this angle must sum exactly to $2\pi$, confirming vanishing deficit on the flat lattice before any curved or weighted analysis.
proof idea
Pure definitional abbreviation: the real is introduced as Real.arccos 0. No lemmas are applied at the definition site. The companion equality to $\pi/2$ is discharged later by Real.arccos_zero.
why it matters
Feeds the flatness gate for the type-(2,2) full-star deficit class kernel. Downstream, flatAngleT22_eq identifies the constant with $\pi/2$, and starFlatAngleSum multiplies by four so the star angle sum is $4\cdot\arccos(0)$. Module doc records the intended identity $4\cdot\arccos(0)=4\cdot(\pi/2)=2\pi$.
In the QG campaign this is deliverable A item 3 (flatness gate) for the (2,2) orbit after the (1,1) seed. It does not finish Hessian assembly over all hinges, nor prove continuum Einstein–Hilbert recovery; it only locks the flat reference angle used by the closed-form 15-class stencil kernel and the subsequent nonvacuity, swap-symmetry, and homothety-stationarity gates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.