flatCos
plain-language theorem explainer
At the flat Freudenthal tetrahedron, the dihedral cosine on local edge slot 0 equals √2/2 exactly. Anyone building the shared flat Regge stencil, angle Jacobian, or first-derivative gate at the cubic six-tet point cites this. The proof is a one-line specialization of the instance's local dihedral-cosine table at index 0.
Claim. For the flat Freudenthal tetrahedron squared-edge tuple, the cosine of the interior dihedral angle at local edge index $0$ equals $\sqrt{2}/2$.
background
This module is Stage 2 (Gate 0 + Lane A) of the Regge TT continuum-symbol campaign in quantum gravity: first-derivative structure of the true nonlinear Regge action on a plane-wave edge field, evaluated at the flat point of a single tetrahedron. Stage 1 already fixed the flat squared-edge stencil every tet of the cubic six-tet Dirichlet complex sees; that stencil is re-exported here as the Freudenthal flat edge tuple.
Regge calculus encodes geometry in edge lengths and deficit angles built from dihedral angles of tetrahedra. The named map that returns the cosine of the 3D dihedral angle from a six-tuple of squared edge lengths, evaluated on that flat Freudenthal tuple at a local edge slot, is the object specialized here. Exact flat cosines are the algebraic input to the closed-form flat angle Jacobian $\partial\theta_f/\partial a_k$ and the flat sqrt-edge derivatives that Gate 0c packages as the shared stencil both continuum lanes must reference.
Sibling facts pin the other five slots: values cycle through $\sqrt{2}/2$, $0$, and $1/2$ only.
proof idea
One-line term proof: apply the physical six-tet cubic Dirichlet instance lemma that tabulates local dihedral cosines on the Freudenthal flat squared-edge tuple, specialized at edge index 0. No further algebraic reduction is performed in this declaration; the equality is inherited from that instance table.
why it matters
Gate 0c of the Regge TT derivative gate needs exact flat dihedral cosines before it can write the flat angle Jacobian and stencil moments used by both continuum lanes. This declaration locks slot 0 to $\sqrt{2}/2$, matching the geometric expectation for the Freudenthal tet in a cubic lattice (right and $45^\circ$-class dihedrals).
It sits inside the proved THEOREM tier of the module: kernel-checked, no sorry, no numerics. It does not touch the still-OPEN continuum TT symbol value (Stage 1 left that as numerical evidence only, target status false) nor second-derivative existence of the plane-wave action profile (Stage 2a). Its role is local and algebraic: feed the shared named stencil so Lane A can deliver first-derivative structure and flat-neighborhood nondegeneracy at a single tet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.