coordPath
plain-language theorem explainer
Defines the one-parameter family of local squared-edge assignments that moves only slot k while freezing the other nine at the flat Freudenthal seed. Anyone proving coordinate derivatives of the seed-hinge dihedral cosine or angle cites this path. The body is a pointwise if-then on Fin 10.
Claim. For each local edge slot $k\in\{0,\ldots,9\}$ and real parameter $t$, the coordinate path is the squared-edge map sending slot $k$ to $t$ and every other slot $j\neq k$ to the corresponding flat Freudenthal squared length.
background
This module sits in the QG full-theory campaign after the flat hinge kernel. It treats the seed triangle hinge inside its two seed-cell Freudenthal 4-simplices, working only with the shared local squared-edge vector of length ten (the incidence layer's local edge mask). The ambient type is SqEdges4, an abbreviation for maps from ten slots to reals: the ten local squared edge lengths in the order fixed by the Freudenthal incidence layer.
The flat reference point is the constant assignment of those squared lengths at the regular Freudenthal seed (both seed simplices share it). Dihedral geometry is packaged as an explicit Gram-projection cosine of the two apex vectors orthogonal to the hinge plane. Differentiating that cosine, and later the angle via arccos, requires a clean one-parameter family through the flat point in each coordinate direction.
The module scope is deliberately narrow: seed hinge only, two seed simplices only; the full lattice orbit sum, the flat Hessian of the 4D Regge action, and EH recovery remain open.
proof idea
Pure definitional construction, not a proof. On input slot index $k$ and real $t$, return the function on Fin 10 that equals $t$ at $j=k$ and equals the precomputed flat seed squared length at every other $j$. No lemmas are applied; downstream derivative theorems simply compose the cosine (or angle) with this path and invoke the generic slot-restriction calculus.
why it matters
This path is the standard probe for deliverable A of the module: all ten flat coordinate derivatives of the seed-hinge dihedral cosine. The master theorem hasDerivAt_cosDihedral_coord and the ten slot lemmas evaluate the cosine along coordPath k, obtaining the kernel values (slot 8 maps to $\sqrt{2}/8$, slot 9 to $-\sqrt{2}/4$, slots 0–7 to 0).
Downstream, the Schläfli-pathwise layer uses it for coordPath_at_seed, the affine identification coordPath_eq_affine, and hasDerivAt_seedDihedralAngle_coord (angle kernel via the flat factor $-1/\sin=-\sqrt{2}$). The second-variation module then quotes the angle derivative along the same path. Without a single shared coordinate path, the ten slot derivatives and the partial-deficit gradient on edge classes (3, 7, 11) would not share a common domain.
It does not close the full Regge Hessian or S_RS_converges_EH_4d; it only supplies the variation curves those later steps need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.