e_020032
plain-language theorem explainer
Pointwise check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (0,2,0,0,3,2). Gravity analysts cite it as one cell of the 4D kernel table. The proof is a single kernel decide on two concrete integers.
Claim. At multi-index $(a,b,c,d,i,j)=(0,2,0,0,3,2)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(0,2,0,0,3,2)$ equals $8$ times the explicit integer kernel value $Z(0,2,0,0,3,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: each term contributes an integer via a local contribution map, summed from zero. The comparison target is an explicit piecewise table $Z$ on the same six indices, returning small integers such as $4$, $-2$, and so on at listed patterns.
The local module is chunk 2 of the identity $m_2^{\mathrm{num}}=8\cdot Z$. The full index space is $4^6=4096$ points; this file discharges a block of those points by kernel decision rather than by a symbolic closed form.
Upstream, $Z$ is the certified explicit table and $m_2^{\mathrm{num}}$ is the fold definition; both live in the kernel-cert module imported here.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values at the fixed six-tuple $(0,2,0,0,3,2)$: the left by evaluating the fold of contributions, the right by looking up the explicit table and multiplying by eight. The kernel checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembled universal statement m2Num_eq_eight_explicitZ, which asserts $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ for every six-tuple in $(\mathrm{Fin},4)^6$. That parent introduces the six indices and splits by fin_cases, so each chunk theorem such as this one closes one concrete cell of the table.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared kernel in 4D: matching the folded coupling sum against eight copies of the closed integer pattern. It does not itself invoke the forcing chain (T5–T8) or the J-cost, but it is part of the certified discrete-gravity substrate those continuum limits sit on.
Sibling e_0200** theorems cover the rest of chunk 2; together they make the assemble step a pure case split rather than an open computation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.