e_122322
plain-language theorem explainer
For the six-index slot (1,2,2,3,2,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}2,d{=}3,i{=}2,j{=}2$ in $\mathrm{Fin}\,4$, the folded 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 Regge exact-midpoint 4D analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling triple at the six Fin-4 indices. The companion map $Z$ is an explicit integer table on those same six indices (pattern-matched cases such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The module is chunk 6 of a 256-way kernel split whose sole job is to certify $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The ambient claim is the universal identity over all $a,b,c,d,i,j:\mathrm{Fin},4$, assembled by exhaustive case split on the six indices.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete Fin-4 tuple $(1,2,2,3,2,2)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (the fold of contributions) and the explicit $Z$ table.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six Fin-4 indices, which is proved by nested fin_cases and dispatches each cell to a chunk decide such as this one. That identity is the algebraic backbone of the Regge exact-midpoint M2TT 4D kernel certificate in the gravity analysis stack. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete kernel bookkeeping needed before continuum or phenomenological gravity claims can cite a certified midpoint numerator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.