e_222130
plain-language theorem explainer
For the six-index slot (2,2,2,1,3,0) on Fin 4, the folded Regge numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one of the 256 pointwise decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=2$, $d=1$, $i=3$, $j=0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated kernel: $m_2^{\mathrm{num}}(2,2,2,1,3,0)=8\,Z_{\mathrm{expl}}(2,2,2,1,3,0)$.
background
This module is chunk 10 of the 256-case kernel certification that the Regge midpoint numerator coincides with eight times an explicit integer table on every six-tuple in $(\mathrm{Fin},4)^6$.
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 contribution term at the given indices. The companion table $Z_{\mathrm{expl}}$ is a sparse pattern-matched map $\mathrm{Fin},4^6\to\mathbb{Z}$ that records the closed-form kernel values (e.g. $\pm 2,,4$ on selected diagonal and off-diagonal slots, zero elsewhere).
The local claim is the single point $(2,2,2,1,3,0)$ of that equality. Upstream definitions live in the KernelCert module; the present file only discharges concrete instances by decision.
proof idea
One-line computational proof: by decide. Lean evaluates both sides as concrete integers (the fold of couplingZList versus eight times the pattern match of explicitZ at these six Fin 4 values) and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
The parent theorem m2Num_eq_eight_explicitZ assembles every Fin 4 six-tuple by nested fin_cases and needs each pointwise equality such as this one. Establishing $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ globally certifies that the midpoint Regge TT identity in 4D reduces to an explicit integer kernel, a necessary algebraic step in the gravity analysis stack of the Recognition Science mirror.
The module header frames the work as "m2Num = 8·explicitZ, chunk 10 (256 kernel decides)"; this declaration is one of those decides. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law, but it hardens the discrete geometric side of the gravity sector that those foundations eventually feed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.