orthCosKernel
plain-language theorem explainer
Lookup table on ten edge slots giving the flat-configuration first derivatives of dihedral cosine under orthogonal length deformations: values ±1/2 on slots 1,3,7,9 and zero elsewhere. Anyone assembling the star deficit linearization or checking HasDerivAt along the orthogonal path cites it. Pure case-split definition, no proof obligations.
Claim. The orthogonal cosine kernel is the map $K_{\mathrm{orth}}:\{0,\ldots,9\}\to\mathbb{R}$ defined by $K_{\mathrm{orth}}(1)=K_{\mathrm{orth}}(9)=-1/2$, $K_{\mathrm{orth}}(3)=K_{\mathrm{orth}}(7)=1/2$, and $K_{\mathrm{orth}}(k)=0$ for every other index.
background
This module builds the full periodic Freudenthal star deficit class kernel for the seed triangle hinge ${0,e_0,e_0+e_1}$ in the 4D integer lattice. Scope is four containing unit cubes and six incident 4-simplices; other hinge orbits remain open. The campaign sits one increment past the two-simplex dihedral cosine calculus and the 15-class edge stencil.
Dihedral cosine is the standard Gram-determinant expression for the angle between two 3-faces meeting at a triangle. Orthogonal coordinate paths vary selected squared edge lengths while holding the flat background fixed, so the first derivative of cosine at the flat point is a pure number per edge slot. The ten slots index the relevant squared-length coordinates in the orthogonal deformation family used by the star analysis.
Sibling data (orthogonal flat squared edges, opposite-orbit Gram pieces) fix the evaluation point; this kernel records only the cosine slopes themselves.
proof idea
Definition by exhaustive pattern match on Fin 10. Four nonzero cases hard-code the constants $\pm 1/2$; the catch-all returns zero. No lemmas, no tactics, no computation.
why it matters
Supplies the numerical derivative payload for the orthogonal family inside the star deficit linearization. Downstream, hasDerivAt_orth_coord states that the derivative of dihedral cosine along each orthogonal coordinate path, evaluated at the flat squared-edge vector, equals this kernel entry. The identity orthDeficitKernel_eq_chain then converts those cosine slopes into deficit-class values via the constant factor $-\mathrm{chainOrth}$.
Together these close the orthogonal half of deliverable A in the module doc: the full-star deficit class kernel on the listed classes, with the listed gates (nonvacuity, swap symmetry, scaling decoy, homothety stationarity). The work does not yet assemble the flat Hessian over all hinges, nor prove continuum EH recovery or flip gap_action_recovery. It is a concrete kernel increment in the QG full-theory campaign, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.