e_123232
plain-language theorem explainer
For the six Fin-4 indices (1,2,3,2,3,2), the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one kernel cell. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}3,d{=}2,i{=}2,j{=}2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer table entry: $\mathrm{m2Num}(1,2,3,2,3,2)=8\cdot\mathrm{explicitZ}(1,2,3,2,3,2)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge midpoint numerator matches a closed table. The ambient goal is the identity m2Num = 8·explicitZ on all six Fin-4 arguments.
The numerator m2Num(a,b,c,d,i,j) is defined by folding contrib over couplingZList, accumulating an Int. The table explicitZ is a pattern-matched Int-valued function on six Fin-4 indices (sample clauses return 4, −2, etc.). Both live in the KernelCert module imported here.
The present declaration fixes one concrete sextuple (1,2,3,2,3,2). Sibling theorems cover the other cells of the same chunk; the assemble theorem recombines them by exhaustive fin_cases.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are literals, so the decidable equality on Int discharges the goal with no lemmas or rewriting.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ in ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which states ∀ (a b c d i j : Fin 4), m2Num = 8 · explicitZ and proves it by six nested fin_cases. Each cell such as this one is a decide obligation generated by that case split.
In the gravity analysis stack this identity is bookkeeping for the exact midpoint form of the 4D Regge M2TT coupling: the folded list definition is interchangeable with the sparse explicit table, scaled by eight. It does not itself invoke the Recognition forcing chain (T0–T8), phi, or the mass ladder; it is pure discrete tensor algebra supporting the Regge side of the RS gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.