e_122000
plain-language theorem explainer
At multi-index (1,2,2,0,0,0) the folded 4D Regge midpoint numerator equals eight times the explicit integer kernel value. Gravity analysts cite this as one atomic case in the 256-point exhaustion of m2Num = 8·Z. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=1,b=2,c=2,d=0,i=0,j=0$ 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 $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis one compares two integer-valued tensors on $(\mathbb{F}_4)^6$. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The comparison target is an explicit piecewise integer kernel $Z$ (tabulated on a handful of ordered sextuples, else implicitly zero in the cert module).
The local module is chunk 6 of a 256-case kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. Upstream, $Z$ and $m_2^{\mathrm{num}}$ are pure definitions; no analytic identity is assumed beyond the tabulated values and the fold.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 sextuple $(1,2,2,0,0,0)$ and checks integer equality. No lemmas are invoked beyond the reducibility of the fold and the explicit $Z$ match.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ exhausts all $a,b,c,d,i,j:\mathbb{F}_4$ by nested fin_cases and dispatches each cell to a chunk identity of this form. This declaration is the cell for $(1,2,2,0,0,0)$. Closing every cell yields the global numerator identity used in the Regge midpoint M2/TT 4D certification path inside the gravity analysis stack. It is bookkeeping, not a new physical law: it pins one lattice point so the assembled equality can be cited without residual cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.