flatAngleJacobianRow0
plain-language theorem explainer
Named constant vector for the flat-angle Jacobian row at face index 0: the six partials ∂θ₀/∂a_k equal (0,0,0,0,−1/4,1/2) in exact rationals. Anyone checking Lane-A3 stencil evaluations or the row-0 smoke test cites it. It is a pure case-split definition, not a derived proof.
Claim. Define the face-$0$ flat-angle Jacobian row as the map $k \mapsto (\partial \theta_0 / \partial a_k)|_{\mathrm{flat}}$ on the six squared-edge coordinates by $k \in \{0,1,2,3\} \mapsto 0$, $k=4 \mapsto -1/4$, and $k=5 \mapsto 1/2$.
background
Module setting is Stage-2 Gate-0 / Lane A of the Regge TT continuum-symbol program: first-derivative structure of the true nonlinear Regge action at the flat Freudenthal tetrahedron, not continuum TT-symbol existence (that target stays open).
The shared named stencil includes the flat squared-edge tuple and the closed-form flat angle Jacobian $\partial\theta_f/\partial a_k$. Face index $f=0$ is the first of the six dihedral angles; edge indices $k=0..5$ run over the six edges of one tetrahedron. At flat geometry the Schläfli radical bridge cancels the arccos $\sqrt{2}$ factor against the $1/\sqrt{32}$ cofactor, so the row collapses to exact rationals.
Sibling material already fixes Gate 0a (plane-wave profile equals true Regge action) and Gate 0b (TT polarizations exist for every integer wave vector). This definition is the concrete row-0 payload that Gate 0c evaluation theorems compare against.
proof idea
No proof body: a six-way pattern match on Fin 6 assigning the six real constants. Downstream evaluation theorems rewrite the computed Jacobian against this table and discharge each coordinate by norm_num plus the Schläfli poly-summand normalization lemmas.
why it matters
Lane A3 needs an explicit, kernel-checkable target for the $f=0$ Jacobian row so that radical cancellation is stated once and reused. The evaluation theorem flatAngleJacobian_row0_eval asserts equality of the computed flat Jacobian to this row; the Bloch-interface audit then uses that equality in row0Smoke_raw_weight_eq_rational to show the raw weight $J_{05}/(2\sqrt{a^*_0})$ is the literal rational $1/4$.
In the QG campaign this is stencil infrastructure, not a continuum claim: the module header keeps the continuum TT symbol value $-(1/4)$ as NUMERICAL EVIDENCE only, and second-derivative existence for stage 2a remains open. The definition simply freezes the exact rational row that those later gates and smoke tests quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.