e_212100
plain-language theorem explainer
For the six-index tuple (2,1,2,1,0,0) on Fin 4, the folded Regge numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 256-point kernel table that underwrites the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,2,1,0,0)$ with each index in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit kernel integer: $m_2^{\mathrm{num}}(2,1,2,1,0,0)=8\,Z_{\mathrm{ex}}(2,1,2,1,0,0)$.
background
This module is chunk 9 of a 256-cell decide table for the 4D Regge midpoint identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$. The ambient setting is exact algebraic certification of a midpoint mass-squared numerator against a closed-form kernel on six Fin-4 indices.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing the local contribution of each coupling term at those indices. The comparison target $Z_{\mathrm{ex}}$ is an explicit integer-valued pattern on the same six indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both objects live in the kernel-cert module imported here; the chunk modules only discharge one concrete equality each.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed at $(2,1,2,1,0,0)$: the fold that defines the numerator becomes a finite integer sum, and explicitZ matches a single pattern clause (or the default). Lean’s kernel decision procedure checks the resulting integer equality; no lemmas are invoked.
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,Z_{\mathrm{ex}}$ by exhausting Fin-4 cases on all six indices. Each chunk cell such as this one supplies one of those 256 residual goals.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge kernel in 4D: it certifies that the folded coupling numerator is a pure multiple of the closed-form $Z$ table, so later curvature and mass-ladder arguments can quote the compact form rather than the fold. It does not itself touch T0–T8 or the RCL; it is infrastructure under the gravity-analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.