e_000000
plain-language theorem explainer
At the all-zero multi-index in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts certifying the 4D Regge exact-midpoint M2–TT identity cite this as one of 256 atomic kernel equalities. The proof is a single decide on concrete integer arithmetic.
Claim. Let $a=b=c=d=i=j=0$ in $\mathrm{Fin}\,4$. Then the folded coupling numerator $m_2^{\mathrm{num}}(0,0,0,0,0,0)$ equals $8$ times the explicit integer kernel $Z(0,0,0,0,0,0)$.
background
This module is chunk 0 of a 256-way case split certifying $m_2^{\mathrm{num}}=8\cdot Z$ on the full $(\mathrm{Fin},4)^6$ index space for the 4D Regge exact-midpoint M2–TT identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at those six indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel-certificate module imported here; the present file only discharges one concrete point of the table.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list versus the pattern match on all zeros), and the kernel decides equality in $\mathbb{Z}$.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the full universal statement
$\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$
by exhausting all six indices with fin_cases; each leaf is one of these chunk equalities (this one is the zero multi-index).
In the Recognition gravity stack, that identity is the algebraic core of the 4D Regge exact-midpoint M2–TT certification: it replaces a folded coupling sum by an explicit sparse integer kernel, enabling exact (non-numeric) checks of the midpoint discrete curvature identities that feed continuum GR limits. It does not itself invoke the forcing chain (T5–T8) or RCL; it is pure discrete-gravity bookkeeping inside the Gravity.Analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.