e_201021
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (2,0,1,0,2,1) equals eight times the explicit kernel entry at those same Fin-4 indices. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ identity. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,1,0,2,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-case kernel certifying the exact midpoint Regge identity for the 4D M2 TT sector: $m_2^{\mathrm{num}}=8\cdot Z$ at every multi-index in $(\mathbb{F}_4)^6$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at the six indices. The comparison object $Z$ is an explicit integer-valued table on the same six Fin-4 arguments (closed-form cases such as $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
The local setting is pure finite enumeration: both sides evaluate to concrete Int values, so each of the $4^6=4096$ slots is in principle decidable; the work is sharded into named one-point lemmas such as this one.
proof idea
One-line kernel proof: decide. Both m2Num 2 0 1 0 2 1 and 8 * explicitZ 2 0 1 0 2 1 reduce to ground integer expressions (fold of a finite list versus a table lookup times eight), and Lean’s decision procedure checks equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and discharges it by exhaustive fin_cases on the six Fin-4 arguments. Each concrete cell such as this one is a leaf of that case tree.
In the broader gravity analysis, the factor-of-eight match between the folded coupling numerator and the explicit kernel is the algebraic content of the exact midpoint M2 TT identity in 4D Regge calculus. Closing the 256-chunk decide kernel removes a scaffolding obligation on that identity and lets downstream curvature or mass-squared arguments quote a fully proved pointwise equality rather than a schematic ansatz.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.