e_312131
plain-language theorem explainer
For the six-index pattern (3,1,2,1,3,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=1$, $i=3$, $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 integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint identity for the M2 numerator: the claim that the folded sum $m_2^{\mathrm{num}}$ equals eight times a sparse explicit integer table $Z$, verified by 256 kernel decides.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and accumulating a local contribution at each tuple. The companion table $Z$ is a pattern-matched integer function on six $\mathrm{Fin},4$ indices (typical nonzero entries are $\pm 2$ or $4$). Both live in the kernel certificate module imported here.
The local setting is pure finite enumeration: every index runs over a four-element type, so each concrete sextuple is a closed integer equality.
proof idea
One-line proof by decide. Lean evaluates both sides of the equality at the fixed indices $(3,1,2,1,3,1)$: the fold that defines the numerator and the pattern match that defines the explicit kernel, then checks the integer identity $m_2^{\mathrm{num}}=8Z$ by computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8Z$ for all six indices, which exhausts $\mathrm{Fin},4$ by nested fin_cases and dispatches each leaf to a chunk equality of this form. That global identity is the algebraic core of the Regge exact-midpoint M2/TT certificate in the gravity analysis stack.
In the Recognition framework this sits inside the discrete gravity side of the forcing chain (spatial $D=3$ and the eight-tick structure enter the broader Regge/midpoint story). The chunk does not itself touch $\phi$-ladder masses or $\alpha$; it only certifies one numerator cell needed for the continuum-limit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.