freudenthal4SimplexFlatDirectionalSchlaefli_coord
plain-language theorem explainer
At the flat Freudenthal 4-simplex seed, the area-weighted sum of dihedral-angle Jacobians over the ten triangle hinges vanishes in every squared-edge coordinate direction. Anyone assembling Gate-A2-style flat directional Schläfli input for 4D Regge calculus cites this. The proof cancels areas against the algebraic Jacobian definition and invokes the already-proved flat column-sum identity.
Claim. For every squared-edge index $k\in\{0,\ldots,9\}$, if $A_h$ is the flat area of hinge $h$ and $J_{h k}$ is the algebraic flat angle Jacobian of hinge $h$ in direction $k$, then $\sum_{h=0}^{9} A_h\, J_{h k}=0$.
background
This module lifts the 3D Gate-A2 Schläfli input (six edges, six face hinges on a tetrahedron) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count equal ten. The local setting is pathwise Schläfli at the flat seed: combinatorics of edges and hinges, strictly positive flat hinge areas, and a closed-form summand table whose columns sum to zero.
hingeAreaFlat h is the Euclidean area of hinge $h$ evaluated on the flat squared-edge triple of that hinge. The algebraic flat angle Jacobian is defined by dividing the flat Schläfli summand by that area: $J_{hk}=S_{hk}/A_h$. Upstream, freudenthal4SimplexFlatSchlaefli already proves that every column of the summand table vanishes: $\sum_h S_{hk}=0$. A private cancellation lemma records $A_h\cdot(x/A_h)=x$ using positivity of the flat areas.
The 3D sibling stencil in ReggeTTDerivativeGate uses the same Jacobian idea for six local edges; here the stencil is ten-by-ten and purely algebraic at flat.
proof idea
Unfold the Jacobian definition so each summand is $A_h\cdot(S_{hk}/A_h)$. Pointwise cancel via mul_div_cancel_area (which needs $A_h>0$), then reassemble the sum with Finset.sum_congr. The resulting bare column sum $\sum_h S_{hk}$ is zero by freudenthal4SimplexFlatSchlaefli k. Short calc, no case splits.
why it matters
This is the Gate-A2-style flat directional Schläfli kill for the 4-simplex: along every affine squared-edge velocity through the flat seed, the area-weighted directional angle sum vanishes. The module tags it as a binding THEOREM and pairs it with the non-vacuous flat SchlaefliIdentityN witness at $n_H=n_E=10$ (strictly positive areas), avoiding the zero-measure shell lesson from 3D.
It sits in the gravity analysis stack that feeds Regge hinge kernels, orbit classification, and flat Hessian assembly. Downstream open items named in the module doc remain: full pathwise identity off the flat seed on Nondeg4Simplex, remapped HasDerivAt for every hinge row, elevation to a candidate, and $S_{RS}\to$ Einstein–Hilbert in 4D. It does not flip gap_action_recovery. No used_by edges are recorded yet; the lemma is the coordinate form of the directional kill that those elevation and convergence goals will need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.