e_202111
plain-language theorem explainer
For the concrete multi-index (2,0,2,1,1,1), the Regge midpoint M2 numerator equals eight times the explicit Z-kernel entry. Gravity analysts cite it as one cell in the 4D kernel table that the assembly theorem exhausts by cases. The proof is a pure `decide` on the evaluated integers.
Claim. For indices $a=2$, $b=0$, $c=2$, $d=1$, $i=1$, $j=1$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on sextuples of Fin 4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contrib rule, and the total is their sum. The comparison target is explicitZ, a sparse case table of small integers (entries such as $4$, $-2$, and so on) that records the closed-form Z kernel at each multi-index.
The local module is chunk 8 of a 256-cell decide grid: each cell asserts $m_2^{\mathrm{num}}=8\cdot Z$ at one concrete sextuple. The identity is the algebraic content of the midpoint M2 TT kernel certificate in four dimensions.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(2,0,2,1,1,1)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold-numerator and the explicit Z table; the kernel is small enough that the decision procedure closes immediately.
why it matters
This cell is consumed by m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on all six Fin 4 arguments. Each chunk theorem such as this one discharges one branch of that case split.
In the broader gravity stack, the factor-of-eight match between the summed coupling numerator and the explicit Z table is the algebraic backbone of the Regge exact midpoint M2 TT identity in 4D. Closing every cell of the 256-grid removes a scaffolding gap in the kernel certificate that later continuum and continuum-limit arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.