t22CosKernel
plain-language theorem explainer
Lookup table of ten real coefficients giving the first derivatives of the hinge-ordered dihedral cosine along each squared-edge coordinate, evaluated at the flat type-(2,2) configuration. Gravity analysts cite it when assembling the star deficit class kernel or proving stationarity of the Regge action on this orbit. The body is a pure pattern-match on Fin 10 with explicit rationals.
Claim. Define a map $K_{\cos}^{(2,2)}:\{0,\ldots,9\}\to\mathbb{R}$ by $K(0)=K(1)=K(4)=-1/4$, $K(2)=K(8)=0$, $K(3)=K(5)=K(6)=K(7)=1/2$, and $K(9)=-1$. These are the partial derivatives of the cosine of the dihedral angle at the type-$(2,2)$ hinge with respect to the ten local squared edge lengths, taken at the flat Gram data.
background
The module treats the full periodic Freudenthal star of one 4D Regge hinge orbit: the type-(2,2) triangle hinge with vertex masks ${0,3,15}$ (difference masks $(3,12)$). Four cube-translate/Kuhn-simplex pairs meet the hinge; each carries a hinge-ordered Gram vector of local squared lengths $(2,4,1,3,2,1,1,3,1,2)$ whose flat dihedral cosine is $0$, so the star angle sum is exactly $2\pi$.
The ten coordinates are the squared edge lengths in hinge order. Differentiating the cosine of the dihedral angle along each coordinate path, at the flat point, produces a ten-slot real vector. That vector is the cosine kernel recorded here. Downstream the deficit kernel is identified with it (chain factor $+1$ on this orbit), and the fifteen-class full-star stencil is assembled by summing over the four star members.
The campaign sits after the type-(1,1) seed orbit and imports the Freudenthal incidence layer, the 15-class edge stencil, and the Gram-projection cosine calculus without redefining their APIs.
proof idea
No proof: the declaration is a total pattern-match on Fin 10 assigning ten explicit rational constants. Each clause is a literal real numeral. Downstream theorems such as hasDerivAt_t22_coord discharge the geometric content by fin_cases on the slot index and citing per-slot derivative lemmas; the definition itself only supplies the target values those lemmas match.
why it matters
This table is the numerical heart of the type-(2,2) star analysis. hasDerivAt_t22_coord states that the derivative of cosDihedral along each coordinate path equals the corresponding entry at the flat squared-edge vector. t22DeficitKernel is defined equal to this map, and t22DeficitKernel_eq_chain records the chain-rule identity with factor $-\mathrm{chain}_{22}=+1$. fullStarClassKernel_eq then unfolds the assembled fifteen-class kernel by summing the four star members against these coefficients.
In the QG full-theory campaign the object is deliverable A item 4: the closed-form full-star deficit class kernel on all 15 stencil classes for this hinge orbit. It does not finish flat Hessian assembly over every hinge, nor prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, nor flip gap_action_recovery. It is the concrete kernel increment after the type-(1,1) seed orbit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.