flatDirectionalAngleDeriv
plain-language theorem explainer
Defines the directional derivative of the h-th hinge dihedral angle at the flat Freudenthal 4-simplex, along any squared-edge velocity v in R^10, as the Jacobian-row contraction Σ_e v_e ∂θ_h/∂ℓ²_e. Anyone proving the flat directional Schläfli identity (Gate A2 at nH=nE=10) cites this. The body is a one-line finite sum against the algebraic flat angle Jacobian.
Claim. For a squared-edge velocity $v \in \mathbb{R}^{10}$ and hinge index $h \in \{0,\ldots,9\}$, the flat directional angle derivative is $\partial_v \theta_h := \sum_{e=0}^{9} v_e \,(\partial \theta_h / \partial \ell_e^2)$ evaluated at the flat Freudenthal seed, where the partials are the algebraic flat angle Jacobian entries (flat Schläfli summand divided by flat hinge area).
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. Work is at the flat seed: squared edge lengths fixed to the regular flat configuration, with strictly positive flat hinge areas hingeAreaFlat.
The algebraic flat angle Jacobian supplies the closed-form partials $\partial\theta_h/\partial\ell_e^2$ at that seed. In this module it is defined as the ratio of the flat Schläfli summand table entry to the corresponding flat hinge area, so that area-weighted contraction recovers the summand table. The 3D sibling in ReggeTTDerivativeGate is the same stencil idea on six local edges: $\partial\theta_f/\partial a_k$ at the flat tet.
Directional angle velocity is the natural object once one passes from coordinate-wise derivatives to an arbitrary affine path $\ell^2(t)=\ell^2_{\mathrm{flat}}+t,v$ through the seed.
proof idea
Pure definition: one finite sum. For fixed hinge $h$ and velocity $v$, contract $v$ against the $h$-th row of the algebraic flat angle Jacobian. No tactics, no lemmas applied at the definition site; downstream proofs unfold this and cancel the area factors against the Jacobian denominator.
why it matters
This is the velocity-side ingredient of the Gate A2-style flat directional Schläfli kill at four dimensions. The parent theorem freudenthal4SimplexFlatDirectionalSchlaefli states that for every $v$, $\sum_h A_h,\partial_v\theta_h=0$, and is proved by unfolding this definition together with the Jacobian-as-summand/area ratio, then invoking vanishing column sums of the flat summand table. The same identity is re-exported as flat_freudenthal_directional_schlaefli for elevation wiring, and appears in the flat directional remainder identity pathwiseFlatRemainder_directional_zero.
Bookkeeping downstream packages the Jacobian (and thus this directional form) into freudenthalFlatVariation, a concrete FlatReggeVariation instance on the 4-simplex seed. Within the module tier tags this closes the THEOREM line "flat directional Schläfli kill along every affine velocity through the flat seed"; it does not address the OPEN pathwise identity off the flat seed on Nondeg4Simplex, nor S_RS_converges_EH_4d.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.