coordPath_at_seed
plain-language theorem explainer
Evaluating the one-parameter squared-edge path that varies only slot k, at that slot's flat-seed value, recovers the full flat seed configuration. Differentiability proofs for the seed-hinge dihedral angle cite this as the base-point identity along each coordinate path. The argument is extensionality plus a two-branch case split on the edge index, discharged by simp.
Claim. For every edge slot $k \in \{0,\ldots,9\}$, if $\gamma_k$ is the path that sets the $k$-th squared edge length to a real parameter $t$ and holds all other slots at the flat Freudenthal seed, then $\gamma_k(s_k)=s$, where $s$ is the full flat seed squared-edge vector and $s_k$ is its $k$-th component.
background
The module develops pathwise Schläfli identities for the Freudenthal (Kuhn) 4-simplex, the 4D analogue of the 3D Gate-A2 closed-form tetrahedron identity. Edge data live in SqEdges4: ten squared lengths indexed by Fin 10, matching $n_H = n_E = 10$.
The flat seed seedFlatSqEdges is the shared Freudenthal squared-length table (values in ${1,2,3,4}$ in local slot order). The coordinate path coordPath k t is the one-parameter family that replaces only slot $k$ by the real $t$ and freezes every other slot at the seed. This lemma records that the path passes through the seed when $t$ equals the seed value in slot $k$.
That base-point fact is the first ingredient in the generic derivative machinery for restrictions of the cosine of the dihedral angle along each slot path.
proof idea
Term-mode proof by function extensionality on the ten edge slots. For each index $j$, case-split on $j = k$. When equal, substitute and unfold the path definition so the varied slot returns $t$ at the seed value. When unequal, the path definition returns the seed entry unchanged. Both branches close by simp on coordPath.
why it matters
Feeds hasDerivAt_seedDihedralAngle_coord, which states that the seed-hinge dihedral angle is differentiable along every squared-edge coordinate path through the flat seed, with derivative angleKernel. That result is a binding THEOREM tier item in the module: the 4-simplex Gate-A2-style input at flat (seed-hinge row matching hinge area times angle kernel).
Without the base-point identity, the chain rule setup for HasDerivAt of seedDihedralAngle \circ coordPath k cannot pin the evaluation point to the flat seed. Downstream this supports flat directional Schläfli kill along affine velocities. It does not close the OPEN items (full pathwise identity off the flat seed, remapped derivatives for every hinge row, elevation to the EH candidate).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.