e_120202
plain-language theorem explainer
For the six-index tuple (1,2,0,2,0,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}0,d{=}2,i{=}0,j{=}2$ in $\{0,1,2,3\}$, the summed 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
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and accumulating each term's contribution at the six indices. The companion map explicitZ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and zeros off the listed patterns).
The module is chunk 6 of a 256-cell kernel certification: each cell asserts $m_2^{\mathrm{num}}=8\cdot Z$ at one concrete six-tuple. The global identity is assembled downstream by exhausting all Fin-4 cases. The setting is pure integer arithmetic on a finite index set; no continuum limit or metric signature is invoked at this layer.
proof idea
One-line decide proof. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted: the fold defining $m_2^{\mathrm{num}}$ evaluates against the coupling list, and explicitZ matches its pattern table (or defaults). Kernel decision procedures discharge the resulting integer equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by fin_cases over all indices and dispatches each cell to a chunk lemma of this form. That global equality is the algebraic core of the Regge-exact midpoint $M_2$ TT identity in 4D within the Gravity analysis stack.
In Recognition Science terms this is bookkeeping infrastructure for discrete curvature/coupling numerics, not a forcing-chain landmark (T5–T8). It closes one of 256 kernel cells so the assembled identity can be cited without residual case obligations. No open physics claim hangs on this single cell alone; its value is exhaustive coverage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.