e_023003
plain-language theorem explainer
For the six-index tuple (0,2,3,0,0,3) on Fin 4, the folded numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts certifying the 4D Regge exact-midpoint M2 TT identity cite this as one atomic kernel cell. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,3,0,0,3)$ with each index 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 value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$. The local setting is the 4D Regge exact-midpoint analysis of the M2 TT identity in the Gravity stack.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $\mathrm{explicitZ}$ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both sides are pure integers once the six indices are fixed, so each cell is a closed arithmetic identity rather than a schematic lemma.
proof idea
One-line proof by decide. After substituting the concrete indices $0,2,3,0,0,3$, both the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $\mathrm{explicitZ}$ reduce to ground integers; the kernel checks $n=8\cdot z$ by computation. No lemmas are invoked beyond the two defining defs.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by nested fin_cases on all six indices; each leaf is one of these chunk cells. Without the pointwise equalities the assembly cannot close.
In the Recognition gravity analysis this identity is the certified numerator form of the 4D Regge exact-midpoint M2 TT kernel: it turns a folded coupling sum into an explicit sparse integer table, which is what downstream curvature and mass-ladder comparisons actually consume. It is bookkeeping infrastructure inside the Gravity domain, not a T0–T8 forcing step, but it is required for any claim that the midpoint M2 kernel matches the explicit $Z$ table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.