e_123010
plain-language theorem explainer
For the six-index tuple (1,2,3,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}3,d{=}0,i{=}1,j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $\mathrm{m2Num}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $\mathrm{explicitZ}(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-cell kernel certification that the Regge midpoint numerator m2Num coincides with eight times a closed-form table explicitZ on every 6-tuple of Fin 4 indices. The local setting is pure integer arithmetic: no continuum limit, only exact equality of two Int-valued maps.
m2Num folds a fixed coupling list, accumulating a contribution at each term for the six indices. explicitZ is the sparse lookup table that records the expected integer (for example 4, -2, or 0) on each admissible pattern. The identity m2Num = 8·explicitZ is the algebraic content of the midpoint M2 TT kernel certificate imported from ReggeExactMidpointM2TTIdentity4DKernelCert.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the decision procedure discharges the equality with no lemmas and no case split inside this declaration. Sibling chunk theorems handle the other index patterns the same way.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six Fin 4 arguments by exhaustive fin_cases and invokes each cell theorem such as this one. That global equality is the certified numerator half of the Regge exact-midpoint M2 TT identity in four dimensions, inside the Gravity analysis track of Recognition Science. It does not itself touch the T0–T8 forcing chain or the J-cost; it is infrastructure for the discrete curvature/mass side of the gravity ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.