farCosKernel
plain-language theorem explainer
Tabulates the ten partial derivatives of the far-orbit dihedral cosine at the flat squared-edge point for the type-(1,2) Regge hinge star. Downstream deficit kernels and star-member assemblies cite it as the linear response of cos(dihedral) under edge-length-squared variations. The body is a pure pattern-match table on Fin 10, with six nonzero cleared-denominator entries and zeros elsewhere.
Claim. Define a map $K_{\mathrm{far}}\colon\{0,\ldots,9\}\to\mathbb{R}$ by $K_{\mathrm{far}}(0)=K_{\mathrm{far}}(1)=-4/(8\sqrt{2})$, $K_{\mathrm{far}}(3)=8/(8\sqrt{2})$, $K_{\mathrm{far}}(5)=K_{\mathrm{far}}(7)=4/(8\sqrt{2})$, $K_{\mathrm{far}}(9)=-8/(8\sqrt{2})$, and $K_{\mathrm{far}}(k)=0$ for all other indices. These are the flat-point partials of the far-orbit dihedral cosine in the ten squared-edge coordinates.
background
The module builds the full periodic Freudenthal star deficit class kernel for the type-(1,2) triangle hinge ${0,e_0,e_0+e_1+e_2}$ (masks $0,1,7$) in 4D Regge calculus on the integer lattice. Scope is two containing unit cubes and four incident 4-simplices; the complement orbit (2,1) and other hinge classes stay open.
Dihedral cosines are computed from Gram data via the committed cleared-denominator pattern imported from the dihedral and flat-kernel layers. Squared edge lengths are organized by a 15-class stencil; a 10-slot far-orbit coordinate path varies those classes while holding the configuration at the flat squared-edge point.
At flatness every simplex cosine is $0$, so the star angle sum is $4\cdot\pi/2=2\pi$. Linear response of cosine under edge variations is the first ingredient of the deficit class kernel (values $\pm\sqrt{2}/2$ after assembly).
proof idea
Pure definition by exhaustive pattern match on Fin 10. Six slots receive explicit rational multiples of $1/\sqrt{2}$ written in cleared-denominator form $(\pm 4$ or $\pm 8)/(8\sqrt{2})$; the remaining four slots are zero. No lemmas or tactics: the table is the content.
why it matters
Feeds the far deficit kernel (identical as a function), the chain-rule identity linking deficit response to $-\mathrm{chainRight}$ times this table, and the derivative certificate that each far coordinate path has derivative equal to the corresponding table entry at the flat point. Private star-member evaluations for members 2 and 3 inline the same numeric coefficients when assembling the full 15-class star kernel.
In the QG campaign this is the type-(1,2) increment after the (1,1) seed orbit: without the far cosine linearization one cannot close flatness gates, nonvacuity, swap symmetry, or homothety stationarity for this hinge class. It does not finish Hessian assembly over all hinges, nor prove continuum EH recovery or flip the gap-action flag.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.