flatAngleJacobian_row0_eval
plain-language theorem explainer
At the flat Freudenthal tetrahedron, the zeroth row of the closed-form dihedral-angle Jacobian equals the explicit rational six-tuple (0, 0, 0, 0, −1/4, 1/2). Lane-A auditors of the Regge TT continuum-symbol program cite this to lock radical cancellation for face index 0. The proof rewrites through the Schläfli-normalized form, then evaluates all six edge cases by direct arithmetic on the Cayley–Menger cofactor polynomials.
Claim. For every local squared-edge index $k\in\{0,\ldots,5\}$, the flat angle Jacobian entry $\partial\theta_0/\partial a_k$ evaluated at the Freudenthal squared-edge tuple equals the $k$-th component of the explicit rational row $(0,0,0,0,-1/4,1/2)$.
background
This module is Stage-2 Gate-0 / Lane A of the Regge TT continuum-symbol campaign: first-derivative structure of the true nonlinear Regge action at the flat point of a single Freudenthal tetrahedron. The shared stencil Jacobian is the closed-form map $\partial\theta_f/\partial a_k$ at the flat squared-edge tuple (three unit steps, two face diagonals, one body diagonal).
Dihedral angles enter through Cayley–Menger cofactors. The explicit polynomial normal form of each cofactor and its partials with respect to squared-edge coordinates supply an algebraic expression for those derivatives. The Schläfli radical bridge rationalizes the arccos summand: up to the common nonzero factor $1/\sqrt{2,\mathrm{cm}_3(a)}$, the summand becomes a pure rational expression, so radicals can cancel against the hinge-area denominator.
An upstream norm lemma already rewrites the $f=0$ row into that rationalized Schläfli form. The present result finishes the evaluation against the named rational target row.
proof idea
One rewrite applies the upstream row-0 norm identity, replacing the closed-form Jacobian entry by its Schläfli-normalized rational expression. A six-way fin_cases on the edge index $k$ then reduces each goal to a concrete real equality. Each case is discharged by norm_num against the explicit definitions of the target rational row, the rationalized Schläfli summand, the Cayley–Menger cofactor polynomials, their partials, and the Freudenthal squared-edge constants. No analytic estimates remain; the arithmetic is finite and exact.
why it matters
Lane A3 of the Regge TT derivative gate needs every flat Jacobian row as exact rationals so stencil moments and Bloch-interface weights stay radical-free. This theorem closes the $f=0$ row: the arccos factor $\sqrt{2}$ cancels against the $1/\sqrt{32}$ cofactor denominator, leaving $(0,0,0,0,-1/4,1/2)$.
Downstream, the Bloch interface audit uses the $k=5$ instance to prove the raw Jacobian coefficient $J_{05}/(2\sqrt{a^*_0})$ equals the literal rational $1/4$. That smoke test is the first concrete rational weight extracted from the shared stencil.
The continuum TT symbol value $-1/4$ and second-derivative existence of the plane-wave action profile remain OPEN; this result only certifies first-derivative structure at flat for a single tetrahedron face.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.