e_020210
plain-language theorem explainer
For the six-index tuple (0,2,0,2,1,0) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise equalities when assembling the global Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}0$, $d{=}2$, $i{=}1$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint analysis, the four-dimensional M2 numerator is built by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums the local contributions of each coupling term at those six Fin-4 indices. The companion table $Z$ is an explicit integer-valued kernel on the same index domain, with sparse nonzero entries such as $4$ or $-2$ on selected patterns.
The module is one chunk of a 256-case decide grid that checks the pointwise identity $m_2^{\mathrm{num}}=8Z$. The local setting is purely combinatorial: both sides are concrete integers once the six indices are fixed, so no continuum limit or curvature hypothesis enters at this layer.
proof idea
One-line decide proof. Lean evaluates both the fold defining $m_2^{\mathrm{num}}$ at $(0,2,0,2,1,0)$ and the matching clause of the explicit kernel $Z$, then checks integer equality with the factor $8$. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which quantifies over all six Fin-4 indices by nested fin_cases and dispatches each cell to a chunk theorem of this form. That global identity is the certified algebraic core of the Regge exact-midpoint M2/TT relation in four dimensions: the folded numerator is exactly eight copies of the closed-form kernel.
Within Recognition gravity, this closes a finite computational obligation rather than a continuum PDE step. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is infrastructure that later curvature and mass-ladder arguments can trust once the midpoint kernel is locked down.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.