pathwiseFlatRemainder_directional_zero
plain-language theorem explainer
For every squared-edge velocity through the flat Freudenthal 4-simplex seed, the pathwise flat remainder (area-weighted directional angle sum minus the double-sum Schläfli contraction) is identically zero. Gravity analysts working Gate-A2-style 4D Regge identities cite it as the remainder form of the flat directional kill. The proof rewrites by the directional Schläfli theorem, then simplifies by vanishing column sums.
Claim. For every velocity $v \in \mathbb{R}^{10}$ on the ten squared-edge coordinates of the flat Freudenthal 4-simplex, $$\sum_{h=1}^{10} A_h^{\mathrm{flat}} \, \partial_v \theta_h - \sum_{e=1}^{10} v_e \Big(\sum_{h=1}^{10} S_{he}^{\mathrm{flat}}\Big) = 0,$$ where $A_h^{\mathrm{flat}}$ is the flat hinge area, $\partial_v \theta_h$ is the directional angle derivative at flat, and $S_{he}^{\mathrm{flat}}$ is the flat Schläfli summand table.
background
This 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 count and the triangle-hinge count equal ten. The local objects are the flat hinge areas $A_h^{\mathrm{flat}}$ (Heron evaluation on the three squared edge lengths of each hinge at the flat seed), the flat Schläfli summand table $S_{he}^{\mathrm{flat}}$, and the directional angle velocity obtained by contracting a squared-edge velocity $v$ against the algebraic angle Jacobian at flat.
Upstream, freudenthal4SimplexFlatSchlaefli proves that every column sum of the summand table vanishes: $\sum_h S_{he}^{\mathrm{flat}} = 0$ for each edge $e$. Its directional contraction, freudenthal4SimplexFlatDirectionalSchlaefli, is the Gate-A2-style statement that the area-weighted directional angle sum itself vanishes for every $v$: $\sum_h A_h^{\mathrm{flat}} \partial_v \theta_h = 0$. The remainder declared here is exactly the difference of those two (already zero) expressions.
proof idea
One-line algebraic cancellation. Rewrite the first sum by freudenthal4SimplexFlatDirectionalSchlaefli v, which replaces $\sum_h A_h^{\mathrm{flat}} \partial_v \theta_h$ by $0$. Then simp with freudenthal4SimplexFlatSchlaefli kills every inner column sum $\sum_h S_{he}^{\mathrm{flat}}$, so the second double sum is likewise $0$. The difference of zeros is zero.
why it matters
Closes the flat directional remainder form of the 4D Schläfli identity on the Freudenthal seed: both the area-weighted angle velocity and the Schläfli double sum vanish separately, so their difference (the pathwise remainder) is identically zero for every affine velocity through flat. This is the 4-simplex analog of the 3D pathwise Schläfli kill used as Gate-A2 input, and it sits inside the module's THEOREM tier for flat directional Schläfli kill.
No downstream consumers are wired yet (used_by is empty). The module still lists as OPEN the full pathwise identity off the flat seed on Nondeg4Simplex, remapped HasDerivAt for every hinge row, elevation to the Regge candidate, and $S_{RS}\to$ Einstein-Hilbert convergence in 4D. The result does not flip gap-action recovery and does not inhabit a vacuous zero-measure Schläfli shell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.