e_002011
plain-language theorem explainer
Kernel equality for multi-index (0,0,2,0,1,1): the midpoint Regge mass-squared numerator equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it only as one cell of the 256-case grid that assembles the full Fin-4 identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,2,0,1,1)$ in $\mathrm{Fin}\,4$, the integer mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local claim is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a $256$-cell grid over $(\mathrm{Fin},4)^6$, discharged by kernel decides.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those six indices. The comparison target $Z$ is an explicit integer-valued kernel on the same six $\mathrm{Fin},4$ arguments, given by a finite case table (e.g. $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The present declaration fixes one concrete cell of that grid: indices $(0,0,2,0,1,1)$.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The proof is the single tactic decide, which runs the kernel decision procedure on the closed integer equality $m_2^{\mathrm{num}}(0,0,2,0,1,1)=8\cdot Z(0,0,2,0,1,1)$. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ and $Z$.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ on all of $(\mathrm{Fin},4)^6$. Its proof introduces the six indices and runs nested fin_cases, so each leaf is exactly one of these chunk equalities.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT kernel in 4D: it certifies that the folded coupling numerator matches the closed-form integer table used downstream. It does not itself touch the forcing chain (T0–T8), $\phi$, or the eight-tick octave; it is pure discrete-kernel certification inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.