e_201030
plain-language theorem explainer
For the six-index slot (2,0,1,0,3,0) on Fin 4, the folded numerator coupling m2Num equals eight times the explicit kernel table entry explicitZ. Gravity analysts verifying the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,0,3,0)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $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 sits in the 4D Regge gravity analysis that checks an exact midpoint identity for the M2TT sector. The local claim of the file is that the folded numerator m2Num equals eight times a sparse explicit kernel table explicitZ, discharged cell-by-cell over the $4^6=4096$ index space in 256-sized decide chunks (this file is chunk 8).
m2Num is the integer obtained by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. explicitZ is a pattern-matched table Fin 4^6 → ℤ that records the closed-form kernel values (typical nonzero entries are $\pm 2,\pm 4$). The identity m2Num = 8·explicitZ is the algebraic content being certified pointwise.
Upstream, both definitions live in the kernel certificate module; this theorem only evaluates them at one concrete multi-index.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the fixed Fin-4 indices to concrete integers (the fold for m2Num and the matching clause or default for explicitZ) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases on all six indices; each leaf is one of these e_* decide cells. Without the chunked kernel equalities, the assemble step cannot close.
In the broader Recognition gravity stack this is bookkeeping for the exact 4D Regge midpoint M2TT identity, not a forcing-chain (T0–T8) step. It locks the discrete curvature/coupling numerator to the explicit kernel so later continuum or continuum-limit arguments can quote a fully certified algebraic identity rather than a numerical check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.