e_010202
plain-language theorem explainer
Pointwise identity: the folded numerator coupling m2Num at discrete indices (0,1,0,2,0,2) equals eight times the explicit integer kernel explicitZ at the same sextuple. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite this as one of 256 kernel cells. The proof is a single kernel decision on both integer sides.
Claim. For the index sextuple $(a,b,c,d,i,j)=(0,1,0,2,0,2)$ with each index in $\mathbb{F}_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 is chunk 1 of a 256-cell kernel certification that the discrete numerator mass-squared coupling equals eight times a closed-form integer table, written $m_2^{\mathrm{num}}=8\cdot Z$, in the 4D Regge exact-midpoint TT analysis.
The numerator side $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each list entry for the six $\mathrm{Fin},4$ indices. The right-hand side is the explicit integer kernel $Z$, a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite case table (e.g. $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
Both sides are pure integers at every concrete sextuple, so each cell is decidable. The present cell fixes the indices $(0,1,0,2,0,2)$.
proof idea
One-line kernel proof: decide evaluates both m2Num 0 1 0 2 0 2 (the fold of contributions) and 8 * explicitZ 0 1 0 2 0 2 (lookup in the explicit table, scaled by eight) as concrete integers and checks equality. No lemmas beyond the definitions of m2Num and explicitZ are required.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the full identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ on $(\mathrm{Fin},4)^6$. Its proof is exhaustive fin_cases on all six indices; each leaf discharges one cell such as this one.
That global identity is the algebraic core of the Regge exact-midpoint M2 TT certification in four dimensions: it replaces a folded coupling sum by an explicit integer kernel, which is what later gravity lemmas need for closed-form midpoint identities. Within Recognition Science gravity analysis this is bookkeeping infrastructure rather than a forcing-chain step (T0–T8), but without the 256-cell cover the midpoint identity does not close in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.