t22CoordPath
plain-language theorem explainer
One-parameter path in squared-edge space for a type-(2,2) Freudenthal 4-simplex: slot k is set to the free real t, and the other nine slots stay at the flat hinge-ordered lengths. Anyone differentiating the dihedral cosine (or deficit class kernel) along a single edge cites this path. The body is a pointwise if-then on Fin 10.
Claim. For each edge index $k\in\{0,\ldots,9\}$ and real $t$, define a squared-length assignment $\ell^2_{k,t}:\{0,\ldots,9\}\to\mathbb{R}$ by $\ell^2_{k,t}(j)=t$ if $j=k$ and $\ell^2_{k,t}(j)$ equal to the flat (2,2) hinge-ordered squared lengths otherwise (namely $(2,4,1,3,2,1,1,3,1,2)$ in local slot order).
background
This module is the type-(2,2) full periodic-lattice star deficit kernel in 4D Regge calculus: the triangle hinge with masks ${0,3,15}$ and its four-simplex Freudenthal star. Squared edge data live in SqEdges4, an abbreviation for maps $\mathrm{Fin},10\to\mathbb{R}$ in the local edge-pair order of the incidence layer.
The flat reference assignment (hinge vertices ordered $(0,3,15)$, apexes by increasing simplex index) is the constant vector with components $(2,4,1,3,2,1,1,3,1,2)$. At that point the Gram-projection cosine of the dihedral angle is zero, so each incident simplex contributes a right angle and the star angle sum is exactly $2\pi$.
Coordinate paths are the standard device for pathwise Schläfli / Hessian work: vary one squared length while freezing the rest at the flat background, then differentiate the cosine (or deficit) in that single slot.
proof idea
Pure definition, not a proof. The value at index $j$ is $t$ when $j=k$ and otherwise the corresponding entry of the flat (2,2) squared-length vector. No lemmas are applied; the body is a single pointwise conditional on $\mathrm{Fin},10$.
why it matters
This path is the domain of every single-slot derivative of the (2,2) dihedral cosine. Downstream, hasDerivAt_t22_coord packages the ten slot theorems (hasDerivAt_t22_slot0 through slot9), each of which applies the cleared-denominator master lemma hasDerivAt_t22_slot along this path and evaluates the derivative of $\cos\theta$ at the flat length in that slot.
Those derivatives feed the full-star deficit class kernel on the 15 stencil classes and the flatness / stationarity gates listed in the module deliverable (nonvacuity, swap symmetries, uniform-scaling decoy, homothety stationarity). In the QG campaign this is the next kernel-checked increment after the type-(1,1) seed orbit; it does not yet assemble the flat Hessian over all hinges or close $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.