coordPath_eq_affine
plain-language theorem explainer
The one-parameter coordinate path that varies only squared-edge slot k equals the affine path through the flat seed with unit velocity in that slot, after a time shift by the seed value. Anyone working the flat directional Schläfli kill or dihedral derivatives along edge coordinates will cite this. The proof is a pointwise case split plus ring arithmetic.
Claim. For each edge slot $k\in\{0,\ldots,9\}$ and real parameter $t$, the coordinate path that sets slot $k$ to $t$ and freezes all other squared edge lengths at the flat Freudenthal seed equals the affine family through that seed with velocity $e_k$ (the standard basis vector in slot $k$), evaluated at the shifted time $t-\ell_k^{\mathrm{flat}}$, where $\ell_k^{\mathrm{flat}}$ is the seed squared length in slot $k$.
background
This module lifts the 3D Gate-A2 Schläfli input to the Freudenthal/Kuhn 4-simplex, where there are ten squared-edge coordinates and ten triangle hinges. The flat seed seedFlatSqEdges is the fixed list of squared lengths $(1,2,3,4,1,2,3,1,2,1)$ shared by the seed simplices in local slot order.
Two path constructions appear. The coordinate path freezes every slot except $k$, setting that slot to the free parameter $t$. The affine path through the flat seed is $\ell_e(t)=\ell_e^{\mathrm{flat}}+t,v_e$ for a fixed velocity $v\in\mathbb{R}^{10}$. Both live in the space of ten squared-edge assignments used by the 4D Regge hinge and Hessian assembly layers.
The equality identifies the coordinate path as the special case of unit velocity in a single slot, after centering the parameter so that $t=\ell_k^{\mathrm{flat}}$ recovers the flat point. That identification is the bridge between the dihedral-kernel derivative machinery (which is written on coordinate paths) and the flat directional Schläfli kill (which is written on affine velocities).
proof idea
Term-mode proof by functional extensionality on the ten edge slots. For each slot $j$, case on whether $j=k$. When $j=k$, both sides reduce to $t$ (left by definition of the coordinate path; right as $\ell_k^{\mathrm{flat}}+(t-\ell_k^{\mathrm{flat}})\cdot 1$). When $j\neq k$, both sides equal the seed value $\ell_j^{\mathrm{flat}}$ (left frozen; right multiplied by velocity $0$). Each case closes by simp unfolding the two path defs and ring.
why it matters
Module tier tags list a THEOREM goal: flat directional Schläfli kill along every affine velocity through the flat seed (Gate A2-style input at flat), plus seed-hinge dihedral HasDerivAt along every squared-edge coordinate path. This lemma is the algebraic glue that lets those two formulations share the same one-parameter families: unit-slot coordinate motion is exactly affine motion with $v=e_k$ after a constant time shift.
No downstream uses are recorded yet in the graph, so the lemma is presently a local identity inside the pathwise Schläfli development. It does not touch the open items (full pathwise identity off the flat seed, remapped derivatives on every hinge row, elevation to the candidate, or $S_{\mathrm{RS}}\to EH$ in 4D), and it does not flip gap_action_recovery. It is pure bookkeeping on the ten-edge squared-length chart at the flat Freudenthal point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.