e_012002
plain-language theorem explainer
For the six-index slot (0,1,2,0,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator at $(0,1,2,0,0,2)$ equals eight times the explicit integer kernel at the same slot: $N(0,1,2,0,0,2)=8\,Z(0,1,2,0,0,2)$.
background
This module is chunk 1 of a 256-cell kernel certification that the Regge midpoint numerator m2Num is identically eight times a sparse explicit table explicitZ. Both live in the 4D kernel certificate: indices run over Fin 4, values are integers.
m2Num a b c d i j is defined by folding a fixed coupling list and summing each term's contribution at those six indices. explicitZ is the closed lookup table that records the nonzero integer values of that sum divided by eight (for example $4$, $-2$, and so on on the diagonal and near-diagonal patterns).
The local goal is purely algebraic bookkeeping: discharge one concrete six-tuple so the assembler can recombine all cells into a universal identity.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,1,2,0,0,2)$: the left via the fold definition of the numerator, the right via the pattern-match table for the explicit kernel scaled by eight. No lemmas beyond kernel evaluation are required.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in Fin 4 by exhaustive fin_cases and invokes each cell theorem such as this one. That universal equality is the numerical spine of the exact midpoint M2 TT identity in the 4D Regge analysis used on the gravity side of the monolith.
In the broader Recognition framework this is infrastructure, not a forcing-chain step: it certifies a discrete curvature/coupling identity so later continuum or continuum-limit arguments can quote a fully discharged integer kernel rather than an open fold. No T0–T8 landmark is proved here; the value is that the gravity stack can treat the eight-fold relation as proved rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.