hasDerivAt_far_coord
plain-language theorem explainer
For each of the ten squared-edge coordinates on the far flat orbit of the type-(1,2) Regge hinge, the dihedral cosine is differentiable in that coordinate at the flat point, with derivative equal to the far cosine-kernel entry. Analysts building the full-star deficit class kernel cite this to justify the first-order stencil on the far orbit. The proof is a Fin-10 case split that invokes the ten single-slot derivative lemmas.
Claim. For every index $k\in\{0,\ldots,9\}$, the map $t\mapsto\cos\theta(\gamma_k(t))$ is differentiable at the far-orbit flat squared-edge vector, and its derivative equals the far cosine-kernel value $\kappa_{\mathrm{far}}(k)$. Here $\gamma_k(t)$ sets the $k$-th squared edge length to $t$ and holds all other edges at their far flat values, and $\cos\theta$ is the Gram-projection cosine of the seed-hinge dihedral inside one 4-simplex.
background
This module treats the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ and its full periodic Freudenthal star in the integer lattice (two unit cubes, four incident 4-simplices). It is the next kernel-checked increment after the type-(1,1) seed orbit. Deliverables include star enumeration, flat cosine multiset, flatness gate (angle sum $2\pi$), and the full-star deficit class kernel on the 15 stencil classes.
The cosine of the seed-hinge dihedral inside one 4-simplex is the committed Gram form $\cos\theta(a)=(\mathrm{apexDot},a)/\sqrt{(\mathrm{apex3NormSq},a)(\mathrm{apex4NormSq},a)}$. The far coordinate path $\gamma_k(t)$ freezes all squared edges at the far flat vector except slot $k$, which is set to the free real parameter $t$. The far cosine kernel supplies the ten target derivative values (nonzero entries are rational multiples of $1/\sqrt{2}$).
Deficit at a hinge is the classical $2\pi-\sum\theta$. Differentiability of $\cos\theta$ along each edge path is the analytic input needed before assembling the linearised deficit stencil on the far orbit.
proof idea
Pure case dispatch on the finite index. fin_cases k splits into the ten inhabitants of Fin 10. Each branch is discharged by the corresponding single-slot lemma hasDerivAt_far_slot0 through hasDerivAt_far_slot9, each of which already proves HasDerivAt of $t\mapsto\cos\theta(\gamma_k(t))$ at the far flat point with derivative equal to the matching kernel entry. No further algebraic work occurs at this layer.
why it matters
The far-orbit half of the type-(1,2) star must contribute a first-order cosine stencil before the full-star deficit class kernel (values $\pm\sqrt{2}/2$ on the 15 classes) can be certified. This theorem packages the ten slotwise derivative facts into one coordinate-indexed statement, matching the near-orbit companion pattern and feeding the kernel assembly and the listed gates (nonvacuity, swap symmetry, uniform-scaling decoy, homothety stationarity).
In the broader QG campaign it is an incremental analytic brick toward flat Hessian assembly over hinges, not a completion of that assembly. It does not touch $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ convergence, gap-action recovery, or reverse-engineered Einstein–Hilbert weights. The complement type-(2,1) orbit and all other hinge orbits remain open. No downstream consumers are recorded yet; the immediate consumer is the full-star deficit class kernel section that follows in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.