e_223212
plain-language theorem explainer
For the six-index tuple (2,2,3,2,1,2) on Fin 4, the folded M2 numerator equals eight times the explicit kernel table entry. Gravity analysts cite it as one of 256 kernel cases assembling the global m2Num = 8·Z identity. The proof is a single decide on concrete integers.
Claim. For indices $a{=}2,b{=}2,c{=}3,d{=}2,i{=}1,j{=}2$ in $\{0,1,2,3\}$, the M2 numerator obtained by folding coupling contributions equals $8$ times the explicit integer kernel value $Z(2,2,3,2,1,2)$.
background
This module is chunk 10 of a 256-case kernel certification that the Regge-exact midpoint M2 numerator matches eight times an explicit integer table on every 4D multi-index.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at those six Fin-4 indices. The companion table $Z$ is a total function Fin 4^6 → ℤ with sparse nonzero patterns (e.g. diagonal blocks 4, off-diagonal −2).
The local claim is the equality at one concrete point of that six-fold index space; sibling theorems cover the other points in the same chunk.
proof idea
One-line computational proof: decide evaluates both sides at the closed indices (2,2,3,2,1,2). The left side reduces the fold of contrib over couplingZList to an integer; the right side looks up explicitZ and multiplies by 8. Equality of the resulting ℤ literals is decided by the kernel.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states ∀ a b c d i j, m2Num = 8 · explicitZ, by exhausting Fin 4 via fin_cases (or by citing the chunk lemmas). That global identity is the certified algebraic core of the Regge-exact midpoint M2/TT analysis in 4D gravity within the monolith.
In the Recognition Science gravity stack this pins a discrete curvature/numerator identity needed for continuum matching; it does not itself invoke the forcing chain (T5–T8) or the J-cost, but sits downstream of the 4D kernel certification imports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.