e_313020
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (3,1,3,0,2,0) equals eight times the explicit integer kernel Z at those indices. Gravity analysts cite it as one of 256 kernel certificates for the 4D Regge midpoint M2–TT identity. The proof is a single decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,3,0,2,0)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel on $(\mathrm{Fin}\,4)^6$.
background
In the 4D Regge midpoint analysis, the M2–TT identity is checked by comparing a folded numerator coupling against a closed-form integer kernel. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing the local contribution of each term at the six Fin-4 indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six indices (typical values $\pm 2,\pm 4$, and so on).
This module is chunk 13 of the 256-point kernel certificate: each chunk discharges one concrete sextuple so the global identity can be assembled by exhaustive case split on $\mathrm{Fin},4$. The local claim is purely arithmetic equality of two integers at one multi-index.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(3,1,3,0,2,0)$. The left side runs the fold that defines the numerator; the right side multiplies the table value of the explicit kernel by 8. No lemmas are invoked beyond the definitions of the numerator and the kernel.
why it matters
Feeds the assembler theorem that states $m_2^{\mathrm{num}}=8Z$ for every sextuple in $(\mathrm{Fin},4)^6$, proved by nested fin_cases over all six indices. That global equality is the algebraic core of the Regge exact-midpoint M2–TT identity in four dimensions, a gravity-side certificate in the Recognition Science stack. The chunking into 256 decide goals keeps each kernel check tiny and machine-checkable; this declaration is the cell for indices $(3,1,3,0,2,0)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.