e_211331
plain-language theorem explainer
For the six Fin-4 indices (2,1,1,3,3,1), the folded M2 numerator equals eight times the explicit Z kernel entry. Gravity analysts cite it as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a pure decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}1$, $d{=}3$, $i{=}3$, $j{=}1$ in $\mathrm{Fin}\,4$, the folded M2 numerator equals eight times the explicit integer Z-kernel value at those indices: $\mathrm{m2Num}(2,1,1,3,3,1)=8\cdot\mathrm{explicitZ}(2,1,1,3,3,1)$.
background
This module is chunk 9 of a 256-cell kernel certification that the Regge exact-midpoint M2 TT identity in 4D holds pointwise: the folded numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, matching the four discrete directions of the 4D lattice.
The numerator m2Num is defined by folding a contribution function over a fixed coupling list, accumulating an integer for each sextuple of indices. The table explicitZ is a pattern-matched integer kernel (typical entries $\pm 2,,4$, and zero off the listed patterns). The local claim is one concrete cell of that comparison.
Upstream, both definitions live in the KernelCert module; the present file only discharges individual decide goals so the assembler can recombine them by exhaustive fin_cases.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the fixed Fin-4 sextuple (2,1,1,3,3,1), reduces the fold that defines the numerator and the pattern match that defines the explicit kernel, and checks integer equality. No lemmas are invoked beyond the decidability of integer equality on closed terms.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity for all six Fin-4 indices and proves it by nested fin_cases, each branch landing on a chunk theorem of this form. This declaration is the cell for (2,1,1,3,3,1) inside chunk 9 of that 256-way split.
In the Recognition gravity stack the identity certifies that the discrete Regge midpoint M2 TT coupling matches the closed-form Z kernel used downstream in curvature and mass-ladder analyses. It is pure linear-algebraic bookkeeping on the 4D index set, not a dynamical claim, but without the cell-by-cell certification the global equality remains unproved in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.