e_203213
plain-language theorem explainer
For the fixed multi-index (2,0,3,2,1,3) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the global m2Num = 8·explicitZ identity over all 4^6 index sextuples. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(2,0,3,2,1,3)$. The summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the folded numerator m2Num equals eight times a closed-form integer table explicitZ, proved by 256 kernel decides.
m2Num a b c d i j is defined by folding a fixed coupling list, accumulating each term's contribution at the six Fin-4 indices. explicitZ is the matching explicit integer function on the 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 local setting is pure integer arithmetic on a finite index set; no continuum limit or physical units enter the certificate itself.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete sextuple $(2,0,3,2,1,3)$ (folding m2Num, looking up explicitZ) and checks integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; N=8Z$ by exhaustive fin_cases on all six indices. Each chunk such as this one discharges one concrete cell so the global identity is a pure case split over decided equalities.
In the gravity analysis stack this identity is the algebraic backbone of the Regge midpoint M2TT kernel certificate in 4D: once numerator and explicit table match everywhere, downstream curvature/mass-coupling identities can quote a single closed form rather than a fold. It is bookkeeping inside the Recognition gravity pipeline, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.