e_200233
plain-language theorem explainer
For the six-index slot (2,0,0,2,3,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 256-point identity that upgrades the midpoint Regge M2TT kernel from a list fold to an explicit integer table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}0,\,d{=}2,\,i{=}3,\,j{=}3$ in $\mathrm{Fin}\,4$, the coupling-fold 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, the M2TT numerator is assembled by folding a fixed coupling list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contribution terms over that list. The companion table $Z$ is an explicit six-argument integer function on $\mathrm{Fin},4$, hard-coded by pattern match (e.g. diagonal-type slots map to $4$ or $-2$).
The local module is chunk 8 of a 256-cell kernel certification: every ordered sextuple in $(\mathrm{Fin},4)^6$ must satisfy $m_2^{\mathrm{num}}=8Z$. That identity turns the fold into a closed lookup used by the exact midpoint gravity certificates.
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the KernelCert module; this chunk only discharges one concrete sextuple.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete Fin-4 indices $(2,0,0,2,3,3)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold and the explicit table; the checker reduces the fold sum and the matched $Z$ entry to numerals and compares.
why it matters
Feeds the universal statement $m_2^{\mathrm{num}}=8Z$ on all of $(\mathrm{Fin},4)^6$ in ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which proceeds by exhaustive fin_cases and dispatches each cell to a chunk theorem of this form. That assembly is the bridge from the coupling-list definition of the midpoint M2TT numerator to the explicit integer kernel used in the 4D Regge gravity analysis.
Within Recognition Science gravity work, the certified kernel supports exact midpoint identities rather than floating-point checks. This declaration is pure scaffolding closure for one of 256 cells; it does not itself touch the T0–T8 forcing chain, but it hardens the discrete geometric side of the gravity stack that those foundations eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.