e_222013
plain-language theorem explainer
For multi-index (2,2,2,0,1,3), the six-index numerator coupling equals eight times the tabulated explicit kernel value. Gravity analysts proving the 4D Regge midpoint M2TT identity cite this as one decided cell in chunk 10 of the 256-kernel case split. The proof is a single computational `decide` on concrete integer arithmetic.
Claim. For indices $a{=}b{=}c{=}2$, $d{=}0$, $i{=}1$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
This module sits in the Gravity analysis layer that certifies an exact midpoint identity for the 4D Regge M2TT kernel. The local setting (module doc) is the claim that the folded numerator equals eight times an explicit table, discharged by 256 kernel decides split into chunks; this file is chunk 10.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list: start at 0 and add contrib t a b c d i j for each term $t$. The explicit kernel $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (sample entries include $Z(0,0,1,1,2,2)=4$ and several $-2$ off-diagonal patterns).
Both definitions live in the KernelCert import. The identity $m_2^{\mathrm{num}}=8Z$ is the algebraic bridge between the summed coupling presentation and the closed-form table used downstream.
proof idea
One-line computational proof: by decide. After substituting the six concrete Fin 4 indices, both sides reduce to closed integers (the fold for the numerator and the matching clause or default of the explicit table), and Lean’s decision procedure checks equality in Int. No lemmas are invoked beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each concrete cell such as this one supplies a decided equality the assembler can close without re-running arithmetic in the big case tree.
In the Recognition gravity stack this is bookkeeping infrastructure for the Regge midpoint M2TT identity in four dimensions, not a forcing-chain landmark (T5–T8) or an RCL step. It earns its place by making the kernel certificate fully machine-checked: every index tuple is pinned, so the eight-factor relation between folded couplings and the explicit table has no residual sorry cells in this chunk.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.