oppDeficitKernel_eq_chain
plain-language theorem explainer
On the seed hinge star, the opposite-orbit deficit kernel equals minus the opposite chain seed times the opposite cosine kernel at the two nonzero class indices 2 and 9. Lattice gravity workers reducing full-star deficit class values to cosine data cite this identity. The proof is a two-case algebraic check after unfolding the three pointwise definitions.
Claim. Let $\sigma^{\mathrm{opp}}=-\sqrt{2}$ be the opposite chain seed, let $c^{\mathrm{opp}}:\{0,\ldots,9\}\to\mathbb{R}$ be the opposite cosine kernel with $c^{\mathrm{opp}}(2)=\sqrt{2}/8$ and $c^{\mathrm{opp}}(9)=-\sqrt{2}/4$, and let $\delta^{\mathrm{opp}}$ be the opposite deficit kernel with $\delta^{\mathrm{opp}}(2)=1/4$ and $\delta^{\mathrm{opp}}(9)=-1/2$. Then $\delta^{\mathrm{opp}}(2)=-\sigma^{\mathrm{opp}}\,c^{\mathrm{opp}}(2)$ and $\delta^{\mathrm{opp}}(9)=-\sigma^{\mathrm{opp}}\,c^{\mathrm{opp}}(9)$.
background
This module is the next kernel-checked increment in the 4D Regge full-theory campaign after the dihedral cosine kernel. It works on the seed triangle hinge ${0,e_0,e_0+e_1}$ and its full periodic Freudenthal star in the integer lattice: four containing unit cubes and six incident 4-simplices. The star is enumerated, flat cosines are read from each orbit Gram vector, and the angle sum is forced to $2\pi$ before any deficit class kernel is written down.
The opposite-orbit data live on a 10-slot class index. The opposite cosine kernel is nonzero only at slots 2 and 9, with values $\sqrt{2}/8$ and $-\sqrt{2}/4$. The opposite deficit kernel is the corresponding pointwise assignment $1/4$ and $-1/2$. The opposite chain seed is the fixed real $-\sqrt{2}$, the scale that converts those cosines into deficits under the star's opposite-orbit geometry.
The local deliverable is the full-star deficit class kernel on classes $(2,3,6,7,10,11,14)$ with values $(-1,-1,+1,-1,+1,+1,-1)$, plus nonvacuity, swap symmetry, and stationarity gates. Other hinge orbits of the lattice remain open.
proof idea
The goal is a conjunction of two equalities, so the proof splits with constructor.
Each branch unfolds the three definitions (opposite deficit kernel, opposite chain seed, opposite cosine kernel) by simp only. The first branch rewrites $-(-\sqrt{2})\cdot(\sqrt{2}/8)$ to $(\sqrt{2}\cdot\sqrt{2})/8$ by ring, applies Real.mul_self_sqrt with the nonnegativity of 2, and finishes by norm_num to $1/4$. The second branch rewrites $-(-\sqrt{2})\cdot(-\sqrt{2}/4)$ to $-(\sqrt{2}\cdot\sqrt{2})/4$ the same way and reduces to $-1/2$. No external lemmas beyond mul_self_sqrt and arithmetic are used.
why it matters
The identity pins the opposite-orbit half of the full-star deficit class kernel to the already-computed opposite cosine multiset and a single geometric seed. That is exactly the reduction needed for deliverable A of the module: a kernel-checked deficit class on the seed hinge star, with values that later feed the nonvacuity, swap-$2\leftrightarrow 3$, uniform-scaling decoy, and homothety stationarity gates.
In the broader Recognition gravity stack this sits inside the Regge 4D campaign that aims at action recovery toward Einstein–Hilbert, without yet claiming $S_{\mathrm{RS}}$ converges to EH in 4D or flipping gap_action_recovery. The module explicitly refuses to reverse-engineer weights from continuum EH. No downstream consumer is wired yet; the lemma is infrastructure for the star kernel itself and for any later assembly that multiplies cosine data by chain seeds rather than hard-coding deficit numbers.
Framework landmarks touched only indirectly: the eight-tick and $D=3$ forcing chain live upstream of the lattice setup; this declaration is pure 4D combinatorial geometry on the Freudenthal star.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.