e_310120
plain-language theorem explainer
For the six-index tuple (3,1,0,1,2,0) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}0$, $d{=}1$, $i{=}2$, $j{=}0$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated kernel entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling term at the six Fin-4 indices. The companion table $Z$ (explicitZ) hard-codes the expected integer kernel values on those same indices (examples in the cert module include $4$, $-2$, and other small integers on selected patterns).
This module is chunk 13 of the exhaustive check that $m_2^{\mathrm{num}} = 8\cdot Z$ on every cell of $(\mathrm{Fin},4)^6$. The local setting is pure integer arithmetic on a finite index set: no continuum limit and no floating-point geometry, only the discrete midpoint kernel used downstream in the M2TT identity assembly.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed: the left-hand side evaluates the fold that defines $m_2^{\mathrm{num}}$, the right-hand side multiplies the matching table entry of $Z$ by eight. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas and no case split inside this declaration.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six indices by fin_cases over $(\mathrm{Fin},4)^6$ and invokes one cell theorem per tuple. Without the cell equalities, the global factor-of-eight relation between the folded numerator and the explicit kernel table cannot be closed.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint M2TT identity in 4D Regge calculus, not a forcing-chain landmark (T5–T8) by itself. It closes one of the 256 discrete kernel obligations so the assembled identity can be cited as a proved integer fact rather than a numeric check outside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.