e_020131
plain-language theorem explainer
At multi-index (0,2,0,1,3,1) the folded M2 numerator coupling equals eight times the explicit Z table entry. Gravity analysts cite it as one kernel cell in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,1,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the M2TT identity is checked pointwise on six Fin-4 indices. The numerator side $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib rule, and the fold starts at 0. The comparison table $Z$ is an explicit six-index integer function with finitely many nonzero patterns (for example diagonal blocks map to 4, mixed pairs to $-2$).
This module is chunk 2 of the 256 kernel decides that discharge $m_2^{\mathrm{num}}=8Z$ cell by cell. The local setting is pure integer arithmetic on a finite index set; no continuum limit or variational argument is invoked here.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete six-tuple $(0,2,0,1,3,1)$ and checks integer equality. The left side reduces by unfolding the fold over couplingZList; the right side multiplies the looked-up explicitZ entry by 8. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ and proves it by exhaustive fin_cases. Each chunk cell such as this one closes one branch of that case split. In the broader gravity stack the identity certifies that the midpoint Regge M2 numerator matches the closed-form Z table used downstream in the 4D TT sector. It is bookkeeping, not a new physical law, but without the full 256-cell cover the assembly theorem does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.