e_201020
plain-language theorem explainer
At multi-index (2,0,1,0,2,0) on (Fin 4)^6, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of 256 pointwise checks that assemble into the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,0,2,0)$ with each coordinate in $\{0,1,2,3\}$, 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
This module is chunk 8 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the 4D Regge midpoint kernel. The ambient setting is discrete gravity analysis: integer-valued couplings on six Fin-4 indices that label edge and simplex data in a 4D triangulation.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the six indices. The comparison target $Z$ is an explicit piecewise-integer table on those same indices (typical values $\pm 2,,4$ on the listed patterns).
The local claim is only the single tuple $(2,0,1,0,2,0)$. Sibling theorems cover the other tuples in the same chunk; the assembly theorem quantifies over all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold of finitely many contributions versus a table lookup, then multiplication by 8), so the kernel closes the equality with no lemmas or rewriting.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ and discharges the universal quantifier by exhaustive fin_cases, invoking one point theorem per tuple. This chunk entry supplies the $(2,0,1,0,2,0)$ cell of that grid.
In the broader gravity stack the identity certifies that the midpoint mass-squared numerator is exactly eight copies of the closed-form Z kernel, a bookkeeping step inside the Regge exact-midpoint analysis rather than a continuum Einstein equation. It does not itself invoke the RS forcing chain (T5–T8), phi-ladder masses, or the alpha band; it is pure discrete-kernel arithmetic supporting the 4D gravity certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.