freudenthal4SimplexFlatDirectionalSchlaefli
plain-language theorem explainer
For any squared-edge velocity through the flat Freudenthal 4-simplex seed, the area-weighted sum of directional dihedral-angle derivatives vanishes. Gravity and Regge analysts cite it as the 4D Gate-A2 flat kill (nH = nE = 10). The proof expands the algebraic Jacobian, cancels positive hinge areas, swaps sums, and invokes the flat column-sum identity.
Claim. For every squared-edge velocity $v \in \mathbb{R}^{10}$ through the flat Freudenthal 4-simplex seed, $\sum_{h=1}^{10} A_h \, (\partial_v \theta_h) = 0$, where $A_h$ is the flat hinge area and $\partial_v \theta_h = \sum_e v_e \, (\partial \theta_h / \partial \ell_e^2)$ is the directional angle derivative from the flat Schläfli Jacobian.
background
This module lifts the 3D Gate-A2 input (tetrahedron, six edges and hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge set and the triangle-hinge set are indexed by Fin 10. The local objects are the flat hinge areas $A_h$ (Heron evaluations on the three squared edge lengths of each hinge at the flat seed) and the rational flat Schläfli summand table $S_{h,e}$.
The algebraic flat angle Jacobian is $J_{h,e} = S_{h,e}/A_h$, and the directional angle velocity along $v$ is $\partial_v \theta_h = \sum_e v_e J_{h,e}$. Upstream, freudenthal4SimplexFlatSchlaefli states that every column of the summand table vanishes: $\sum_h S_{h,e} = 0$ for each edge $e$. Areas are strictly positive, so division by $A_h$ is legitimate (mul_div_cancel_area).
The module tags this as the flat directional Schläfli kill along every affine velocity through the flat seed, the 4D analog of the 3D pathwise Schläfli evaluation along edge directions.
proof idea
Tactic proof by calc after unfolding the directional derivative and Jacobian. First rewrite the weighted sum as a double sum $\sum_h \sum_e v_e S_{h,e}$ by distributing multiplication over the inner sum and cancelling each $A_h$ against the denominator via mul_div_cancel_area. Commute the finite sums and factor $v_e$ to obtain $\sum_e v_e (\sum_h S_{h,e})$. Each inner column sum is zero by freudenthal4SimplexFlatSchlaefli, so the whole expression collapses to $\sum_e v_e \cdot 0 = 0$.
why it matters
This is the Gate-A2-style flat directional contraction of the closed-form column-sum theorem, and the module lists it among the binding THEOREM tags for 4D pathwise Schläfli. Downstream, flat_freudenthal_directional_schlaefli re-exports it for elevation wiring in the second-variation analysis, and pathwiseFlatRemainder_directional_zero uses it to show the flat directional remainder vanishes for every velocity.
In fold bookkeeping it supplies the inhabited Schläfli premise for freudenthalFlatVariation: the flat 4-simplex seed is a concrete real instance of the variation data (areas, Jacobian, velocities), so the premise is not a vacuous zero-measure shell. That feeds decoy-factor comparisons and the broader program toward $S_{\mathrm{RS}}$ converging to Einstein–Hilbert in 4D.
Open items remain off-seed: full pathwise identity on nondegenerate 4-simplices, remapped HasDerivAt for every hinge row, and elevation to the candidate action. This result does not flip gap-action recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.