e_220101
plain-language theorem explainer
At the single index sextuple (2,2,0,1,0,1) in (Fin 4)^6, the folded Regge midpoint numerator equals eight times the explicit integer kernel table. Gravity analysts cite it as one of 256 concrete kernel checks that assemble into the global m2Num = 8·explicitZ identity. The proof is a pure `decide` on ground integers.
Claim. For indices $a{=}2,\,b{=}2,\,c{=}0,\,d{=}1,\,i{=}0,\,j{=}1$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 10 of a 256-way case split proving that the Regge midpoint $m_2$ numerator coincides with eight times a closed-form integer table on every sextuple of indices in $\mathrm{Fin},4$. The local setting is exact discrete gravity bookkeeping: no continuum limit is taken here.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a contribution functional at the six indices. The table $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (typical values $\pm 2,,4$, and sparse support). Both live in the kernel certificate module imported by this chunk.
The global claim is the pointwise identity $m_2^{\mathrm{num}}=8Z$ for all indices; each chunk theorem discharges one concrete sextuple so the assembler can finish by exhaustive fin_cases.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel decision procedure closes the equality with no lemmas and no arithmetic rewriting by hand.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, dispatching each goal to a chunk equality of this form.
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge analysis in 4D: it certifies that the folded coupling numerator is a pure multiple of the sparse explicit kernel, so later curvature or mass-ladder arguments can quote the closed table instead of the fold. It does not itself invoke T5–T8 or the RCL; it is a finite combinatorial certificate underneath those continuum-facing claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.