e_201022
plain-language theorem explainer
For the six-index slot (2,0,1,0,2,2) on Fin 4, the folded numerator coupling equals eight times the tabulated explicit kernel entry. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one atomic kernel cell. The proof is a pure `decide` on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $N$ for the folded numerator coupling obtained by summing all list contributions at those indices, and $Z$ for the explicit integer kernel table. Then $N(2,0,1,0,2,2)=8\,Z(2,0,1,0,2,2)$.
background
This module sits in the Gravity analysis stack for the exact midpoint form of the 4D Regge M2–TT identity. The local contract, stated in the module header, is to discharge one chunk of the pointwise claim $N=8Z$ by kernel decision (256 cells per chunk).
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution at the six Fin-4 indices. The table $Z=\mathrm{explicitZ}$ is a closed-form integer function on $(\mathrm{Fin},4)^6$, with sparse nonzero cases such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns.
Upstream, both $N$ and $Z$ live in the KernelCert module; this file only instantiates one concrete six-tuple and checks the scalar identity.
proof idea
One-line kernel proof: by decide. Lean reduces both sides to concrete Int values (the fold for $N$ at $(2,0,1,0,2,2)$ and the matching explicitZ clause, scaled by 8) and closes by decidable equality on integers. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhaustive fin_cases on all six indices. Each case obligation is exactly one of these chunk theorems; this declaration discharges the cell $(2,0,1,0,2,2)$ inside chunk 8.
In the broader RS gravity line, the identity underwrites the exact midpoint M2–TT kernel used in 4D Regge analysis. It is bookkeeping infrastructure rather than a forcing-chain step (not T0–T8), but without the pointwise $N=8Z$ match the assembled continuum identity does not typecheck.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.