pathwiseFlatRemainder_flat_zero
plain-language theorem explainer
On the flat Freudenthal 4-simplex seed, the candidate Jacobian formed by dividing each flat Schläfli summand by the corresponding flat hinge area makes the pathwise remainder vanish in every edge direction. Anyone assembling Gate-A2-style flat directional Schläfli input in 4D cites this. The proof cancels areas against the denominators, then invokes the known vanishing of flat column sums.
Claim. Let $a$ be the flat squared-edge assignment on the Freudenthal 4-simplex, and let $\partial\theta_{h,e}$ be the candidate directional table $\partial\theta_{h,e} = S_{h,e}/A_h$ where $S_{h,e}$ is the flat Schläfli summand and $A_h>0$ is the flat hinge area. Then for every edge index $e\in\{0,\ldots,9\}$, $\sum_h A_h(a)\,\partial\theta_{h,e} - \sum_h S_{h,e} = 0$.
background
This module lifts the 3D Gate-A2 Schläfli closed form (six edges, six hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count equal ten. Squared edge lengths live in SqEdges4; the flat seed flatSqEdges is the regular Euclidean configuration used as the expansion point.
Hinges are triangles. Each hinge $h$ has three boundary edge slots; its Euclidean area is computed by Heron from those three squared lengths. On the flat seed those areas specialize to strictly positive constants hingeAreaFlat h. The flat Schläfli summand table $S_{h,e}$ records the closed-form contribution of hinge $h$ to edge coordinate $e$ at flat; its column sums vanish by freudenthal4SimplexFlatSchlaefli.
PathwiseFlatRemainder a dTheta is the residual that compares a candidate Jacobian $d\Theta$ against that flat table: for each edge velocity $e$, the area-weighted sum of $d\Theta_{h,e}$ must equal the flat column sum. Vanishing of the remainder is the flat directional Schläfli identity used as Gate-A2 input.
proof idea
Fix an arbitrary edge index $e$. Invoke freudenthal4SimplexFlatSchlaefli e, which states that $\sum_h S_{h,e}=0$.
It remains to show that the area-weighted sum with $d\Theta_{h,e}=S_{h,e}/A_h$ collapses to the bare sum of summands. Pointwise, the hinge area evaluated on the flat seed equals hingeAreaFlat h by definition, so each term is $A_h\cdot(S_{h,e}/A_h)$. Since $A_h>0$ (hingeAreaFlat_pos), field_simp cancels the ratio and the Finset sum becomes $\sum_h S_{h,e}$.
Rewrite the remainder as that identity followed by the vanishing column sum, then sub_self yields zero.
why it matters
Module tier tags list as THEOREM the flat directional Schläfli kill along every affine velocity through the flat seed (Gate A2-style input at flat). This declaration is exactly that kill for the normalized flat Jacobian: it certifies that dividing the closed-form summand table by flat hinge areas produces a remainder-free directional form on the seed.
It sits downstream of the flat closed-form column-sum theorem and the positive flat hinge-area lemmas, and upstream of the still-open pathwise identity off the flat seed on nondegenerate 4-simplices, the full remapped HasDerivAt for every hinge row, elevation to a Regge candidate, and eventual $S_{RS}\to$ Einstein-Hilbert convergence in 4D. It does not touch gap-action recovery.
In the broader Recognition gravity stack this is the 4D analogue of the tetrahedron six-edge Schläfli closed form: a non-vacuous flat witness with strictly positive areas, avoiding the zero-measure shell pathology flagged in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.