e_010020
plain-language theorem explainer
For the six-index slot (0,1,0,0,2,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 256-way kernel certification of the Regge midpoint M2TT identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,0,2,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel: $m_2^{\mathrm{num}}(0,1,0,0,2,0)=8\,Z_{\mathrm{explicit}}(0,1,0,0,2,0)$.
background
In the 4D Regge midpoint analysis, the M2TT identity is checked by comparing a folded numerator against a closed-form integer kernel. The numerator m2Num sums contrib terms over couplingZList for six Fin 4 indices. The kernel explicitZ is a pattern-matched integer table on those same indices (typical nonzero entries are $\pm 2$ or $4$).
This module is chunk 1 of the 256 kernel decides: each declaration fixes one multi-index and asserts m2Num = 8 · explicitZ at that point. The local setting is pure integer equality on a finite domain, not continuum GR.
proof idea
One-line decide. Both sides reduce to concrete Int values for the fixed indices $(0,1,0,0,2,0)$, so the kernel decision procedure discharges the equality with no lemmas or rewriting.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ by exhausting all $4^6$ index tuples. That global identity is the certified algebraic core of the Regge exact-midpoint M2TT check in four dimensions. Without the per-slot decides, the assembler cannot close. It is bookkeeping inside the gravity analysis stack, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.