PathwiseFlatRemainder
plain-language theorem explainer
Predicate on squared edge lengths and a candidate dihedral Jacobian: area-weighted hinge sums must match the flat Schläfli summand table edgewise. Gravity analysts cite it as the Gate-A2 flat remainder at the Freudenthal 4-simplex (10 hinges, 10 edges). Pure definitional Prop; no proof content.
Claim. Let $a$ be squared edge lengths on the Freudenthal 4-simplex ($10$ slots) and let $d\theta_{h,e}$ be a candidate table of dihedral derivatives. The pathwise flat remainder vanishes when, for every edge index $e$, $\sum_{h=0}^{9} A_h(a)\, d\theta_{h,e} - \sum_{h=0}^{9} S^{\mathrm{flat}}_{h,e} = 0$, where $A_h(a)$ is the Heron hinge area from the three boundary edges of hinge $h$, and $S^{\mathrm{flat}}$ is the precomputed flat Schläfli summand table.
background
The module lifts the 3D Gate-A2 Schläfli input (tetrahedron, six edges/hinges) to the Freudenthal/Kuhn 4-simplex, where both the edge count and the triangle-hinge count equal ten. Squared lengths live in SqEdges4 ($\mathrm{Fin},10\to\mathbb{R}$). Each hinge $h$ has three boundary edge slots given by hingeBoundarySlots, ordered $(v_0v_1,v_0v_2,v_1v_2)$.
Hinge area is the Heron square-root $A(a,b,c)=\sqrt{\mathrm{heronSq}(a,b,c)}$ from the flat Hessian assembly. The flat Schläfli summand table $S^{\mathrm{flat}}_{h,e}$ is the closed-form contribution of hinge $h$ to edge coordinate $e$ at the flat seed. The module already proves column sums of that table vanish and that the seed-hinge row matches area times the dihedral angle kernel.
Local setting: pathwise Schläfli identities along affine edge paths through the flat seed, as directional input to Regge calculus in 4D.
proof idea
Definitional Prop, not a theorem. The body is a single universal quantifier over edge indices $e\in\mathrm{Fin},10$: form the area-weighted sum of the candidate Jacobian $d\theta_{h,e}$ over the ten hinges, subtract the sum of flat Schläfli summands, and require equality to zero. Areas are evaluated on the three boundary squared lengths of each hinge via hingeBoundarySlots. No tactics or lemmas are invoked.
why it matters
Supplies the exact remainder predicate that pathwiseFlatRemainder_flat_zero discharges at the flat seed, taking $a$ to be the flat squared lengths and $d\theta_{h,e}=S^{\mathrm{flat}}_{h,e}/A_h^{\mathrm{flat}}$. That theorem is the Gate-A2-style flat directional Schläfli kill for the 4-simplex.
In the module tier list this sits under the proved flat directional Schläfli package (column sums, seed-hinge HasDerivAt, non-vacuous positive-area witness). It does not close the open pathwise identity off the flat seed on Nondeg4Simplex, nor the elevation-to-candidate or $S_{RS}\to EH$ convergence goals. Framework role: discrete curvature bookkeeping for 4D Regge gravity inside the Recognition stack; no direct T0–T8 or $\phi$-ladder content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.