flatAngleJacobian
plain-language theorem explainer
Algebraic Jacobian of hinge dihedral angles with respect to squared-edge coordinates, evaluated at the flat Freudenthal 4-simplex seed. Anyone proving the flat directional Schläfli kill or assembling flat Regge variation data cites it. The body is the quotient of the flat Schläfli summand by the flat hinge area, the 4D analog of the shared 3D stencil Jacobian.
Claim. For hinge index $h$ and edge index $e$ ranging over $\{0,\ldots,9\}$, the flat angle Jacobian is $J_{h,e} := S_{h,e}/A_h$, where $S_{h,e}$ is the flat Schläfli summand and $A_h$ is the area of hinge $h$ at the flat seed (strictly positive).
background
The module lifts the 3D Gate-A2 Schläfli input (six edges, six hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the edge set and the triangle-hinge set have cardinality 10. At the flat seed one has a rational table of Schläfli summands and strictly positive hinge areas obtained from the three squared edge lengths of each triangular hinge via the usual Heron formula.
The 3D precursor in the TT derivative gate defines the shared stencil Jacobian as the closed-form partial $\partial\theta_f/\partial a_k$ of a local dihedral angle with respect to a local squared-edge coordinate at the flat Freudenthal tetrahedron. The present definition is the same algebraic object at $n_H=n_E=10$: summand over area, so that area-weighted contraction recovers the summand table whose columns vanish.
Local notation: hinges and edges are indexed by Fin 10; areas come from hingeAreaFlat; summands from the rational flat table cast to $\mathbb{R}$.
proof idea
Pure definition: the real quotient of the flat Schläfli summand at $(h,e)$ by the flat hinge area of $h$. No tactics; the non-vanishing of the denominator is supplied later by the positivity lemma on flat hinge areas when the definition is unfolded in theorems.
why it matters
This Jacobian is the algebraic engine of the flat directional Schläfli kill. Downstream, flatDirectionalAngleDeriv contracts it against an arbitrary squared-edge velocity; freudenthal4SimplexFlatDirectionalSchlaefli then proves that the area-weighted sum of those directional angle velocities vanishes for every velocity through the flat seed (Gate A2-style at flat, the 4D analog of the 3D pathwise kill). The coordinate form of the same identity is the column-sum vanishing of the summand table after cancelling areas.
The seed-hinge row is identified with the existing angle kernel from the 4D dihedral kernel module. Fold bookkeeping packages the Jacobian into a concrete FlatReggeVariation instance, and the TT Bloch audit reuses the same stencil coefficients in raw cell terms. The module still leaves open the full pathwise identity off the flat seed on nondegenerate 4-simplices and the elevation to the continuum EH candidate; this definition does not touch those gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.