e_123200
plain-language theorem explainer
Pointwise check that the folded M2 numerator coupling equals eight times the explicit Z-table entry at multi-index (1,2,3,2,0,0). Gravity analysts assembling the 4D Regge midpoint M2TT identity cite these 256 kernel chunks. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,3,2,0,0)$ in $(\mathbb{F}_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, two integer-valued maps on six $\mathbb{F}_4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local kernel, and the fold starts at zero. The comparison target is an explicit case table $Z$ that returns a small integer (typically $\pm 2$ or $4$) on selected index patterns and is used as a closed-form certificate.
This module is chunk 6 of the 256-point kernel certification that $m_2^{\mathrm{num}}=8Z$ holds at every multi-index. The local setting is pure finite enumeration: no continuum limit or curvature hypothesis enters the equality itself.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(1,2,3,2,0,0)$. The left side reduces by unfolding the fold over the coupling list; the right side multiplies the table lookup by eight. Equality of the resulting integers is discharged by the kernel decision procedure.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk theorem per residue class. Closing the full identity certifies the algebraic midpoint M2TT relation used in the discrete gravity analysis. Landmark contact is indirect: the certified coupling structure sits inside the RS gravity stack that ultimately ties to the forced $D=3$ spatial sector (T8) and the eight-tick discrete time skeleton (T7), but this lemma itself is only a finite integer identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.