e_311212
plain-language theorem explainer
Equates the folded Regge midpoint m2-numerator at multi-index (3,1,1,2,1,2) to eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a pure `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,1,2,1,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib, and the fold starts at $0$. The comparison target explicitZ is a sparse case table of small integers (entries such as $4$, $-2$, and so on) that records the closed-form kernel.
This module is chunk 13 of a 256-cell partition of the $(\mathrm{Fin},4)^6$ domain. The local claim is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ at one fixed multi-index. The factor $8$ is the universal scaling that matches the folded sum to the tabulated kernel across the whole grid.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The proof is the single tactic decide, which reduces the equality of those integers by computation. No algebraic lemmas are invoked beyond the definitions of the fold and the case table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$. Its proof runs fin_cases on all six indices and discharges each cell; this declaration is the cell for $(3,1,1,2,1,2)$. Together the 256 chunk theorems certify that the folded coupling numerator is exactly eight times the explicit Z kernel, a computational certificate inside the Regge midpoint $M_2$ TT-identity analysis in the Gravity domain of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.