starFlatCosines_match_orbit
plain-language theorem explainer
On the type-(2,2) Regge hinge star, every flat cosine entry equals the dihedral cosine of the flat squared-edge data. Anyone assembling the four-simplex star angle sum or the flatness gate cites this. The proof is a one-line term that symmetrizes the already-proved vanishing of that dihedral cosine.
Claim. For every star index $m\in\{0,1,2,3\}$, the flat cosine assigned to member $m$ equals the dihedral cosine of the type-$(2,2)$ flat squared-edge configuration (both sides equal $0$).
background
This module treats the type-(2,2) triangle hinge ${0,e_0+e_1,e_0+e_1+e_2+e_3}$ (masks ${0,3,15}$) and its full periodic Freudenthal star in 4D Regge calculus. The star has exactly four incident (cube translate, Kuhn simplex) pairs.
The dihedral cosine of a seed hinge inside one 4-simplex is the Gram-projection ratio of apex dot product over the product of apex 3- and 4-norms. The local flat squared-edge vector for this orbit is fixed; its dihedral cosine vanishes. The star flat-cosine table is the constant-zero map on four indices, matching the pattern used for other hinge orbits (type (1,1), (1,2), (1,3)) with their own constant or two-value tables.
Upstream, the vanishing identity for the type-(2,2) flat dihedral cosine is already kernel-checked by cleared-denominator reduction and numeric simplification of the Gram data.
proof idea
One-line term proof: apply symmetry of the upstream vanishing theorem that the dihedral cosine on the type-(2,2) flat squared edges equals zero. The star flat-cosine definition is the constant-zero function on Fin 4, so both sides match for every index.
why it matters
Closes the flat-cosine multiset step of deliverable A in the type-(2,2) star kernel: all four incident simplices carry flat cosine $0$. That feeds the flatness gate (star angle sum $4\cdot\arccos 0=2\pi$) and the full-star deficit class kernel on the 15 stencil classes.
It sits in the QG full-theory campaign after the type-(1,1) seed orbit, reusing the Freudenthal incidence layer and Gram-projection cosine calculus without redefining their API. No downstream consumers are wired yet in the graph; the immediate parent goals remain the flat Hessian assembly and, farther out, $S_{\mathrm{RS}}$ convergence to Einstein–Hilbert in 4D, neither of which this lemma claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.