flatCos_value_cases
plain-language theorem explainer
On the Freudenthal flat tetrahedron, each of the six dihedral cosines equals exactly one of √2/2, 0, or 1/2. Anyone bounding flat angles or building the Regge TT stencil Jacobian cites this case split. The proof is a Fin-cases exhaustion that plugs in the six precomputed flat-cosine identities.
Claim. For every edge index $f \in \{0,\ldots,5\}$, the tetrahedral dihedral cosine of the Freudenthal flat squared-edge tuple at $f$ equals $\sqrt{2}/2$, or equals $0$, or equals $1/2$.
background
This module is Stage-2 Gate-0 / Lane-A of the Regge TT continuum-symbol program: first-derivative structure of the plane-wave Regge action at the flat Freudenthal tetrahedron, not the continuum TT symbol itself (that target stays open).
The squared-edge data freudenthalTetSqEdges is the local flat tuple every Freudenthal tet in the unit cube sees: three unit steps, two face diagonals, and one body diagonal (values $1,2,3,1,2$ on the five listed slots, completing the six-edge Cayley–Menger input). The cosine dihedralCos3Sq is the tetrahedral dihedral cosine extracted from Cayley–Menger cofactors: cofactor of the opposite vertex pair over the matching denominator.
The six named flat-cosine lemmas (flatCos₀…flatCos₅) already evaluate that cosine edge-by-edge on the Freudenthal tuple; this theorem packages them as a single trichotomy over Fin 6.
proof idea
Term-mode exhaustion: fin_cases f splits into the six edge indices. Each branch is a one-line exact of the matching precomputed identity, wrapped in the appropriate Or.inl / Or.inr nesting so the disjunction is √2/2 ∨ 0 ∨ 1/2. No further algebra runs here; the numerical content lives in flatCos₀–flatCos₅.
why it matters
Feeds flatCos_bounds, which upgrades the trichotomy to the strict enclosure $-1 < \cos < 1$ needed for nondegenerate flat angles (arccos domain, nonzero angle Jacobian factors). That bound is part of Gate 0c’s shared named stencil: flat angle Jacobian $\partial\theta_f/\partial a_k$ and flat sqrt-edge derivatives on freudenthalTetSqEdges, which both TT lanes must reference.
In the QG campaign this is pure THEOREM infrastructure for Lane A first-derivative structure at a single flat tet. It does not touch the open continuum TT symbol value (still numerical evidence only, target flag false) nor second-derivative existence of the plane-wave action profile (stage 2a). Landmark contact is geometric scaffolding for discrete gravity, not the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.