e_212310
plain-language theorem explainer
For the index sextuple (2,1,2,3,1,0) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel cells that assemble the global identity m2Num = 8·explicitZ. The proof is a pure decide on concrete integers.
Claim. For indices $a=2,b=1,c=2,d=3,i=1,j=0$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel entry $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis the 4D TT identity is reduced to a finite kernel on six indices in $\mathrm{Fin},4$. The numerator side $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at each sextuple. The comparison object explicitZ is a sparse integer table that records the closed-form kernel values on those same indices (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$ and sign-flipped off-diagonal pairs $\mapsto -2$).
This module is chunk 9 of the 256-cell decide grid that discharges $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure integer arithmetic: no continuum limit or curvature hypothesis enters the cell proofs.
proof idea
One-line decide. Both sides evaluate to concrete integers once the six Fin-4 arguments are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern-match definition of explicitZ; Lean’s kernel decision procedure checks equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which universally quantifies over all six Fin-4 indices by nested fin_cases and invokes each cell (including this one) as a leaf. That global identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in 4D gravity analysis: it converts the folded coupling sum into an explicit sparse kernel, enabling exact rather than approximate midpoint identities. Within Recognition Science gravity work this is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but it is required before continuum or continuum-limit claims can rest on a fully certified discrete kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.