e_210030
plain-language theorem explainer
For the multi-index tuple (2,1,0,0,3,0), the midpoint Regge numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite these 256 atomic equalities when assembling the global 4D identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2$, $b{=}1$, $c{=}0$, $d{=}0$, $i{=}3$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded midpoint 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
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at each multi-index. The companion $Z$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
The module is chunk 9 of a 256-case kernel certification: each chunk proves $m_2^{\mathrm{num}}=8Z$ at one concrete index tuple. The ambient claim is the pointwise identity of these two kernels on the full $4^6$ grid, which underpins exact midpoint identities used in the discrete gravity sector.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed indices $(2,1,0,0,3,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and explicit $Z$ (table lookup).
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8Z$ for all six indices, which runs fin_cases over $a,b,c,d,i,j$ and dispatches each cell to a chunk equality of this form. That global identity is the certified algebraic core of the Regge exact-midpoint $M_2$ TT analysis in 4D. Within Recognition gravity, such kernel equalities lock the discrete curvature bookkeeping before continuum or phenomenological limits are taken; they do not themselves invoke the forcing chain (T5–T8) or the mass ladder, but they stabilize the geometric side those landmarks later couple to.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.