e_123302
plain-language theorem explainer
At the six Fin-4 indices (1,2,3,3,0,2), the folded coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts building the 4D Regge midpoint M2TT identity cite this as one concrete kernel-point check among the 256-case split. The proof is a single decide on ground integer arithmetic.
Claim. For indices $a=1$, $b=2$, $c=3$, $d=3$, $i=0$, $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 value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-way split proving that the folded numerator m2Num equals eight times an explicit integer table explicitZ, pointwise on Fin 4^6. The local setting is the 4D Regge midpoint M2TT identity kernel certification in the Gravity analysis stack.
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 arguments (sample clauses include (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ -2). Both live in the KernelCert import.
The equality m2Num = 8·explicitZ is the algebraic content being certified case-by-case before reassembly.
proof idea
One-line kernel decision: by decide. Both sides reduce to concrete Ints once the six Fin 4 literals are substituted into m2Num (the fold of contrib over couplingZList) and explicitZ (the pattern match). Lean’s decide tactic closes the resulting integer equality with no further lemmas.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ in ReggeExactMidpointM2TTIdentity4DM2NumAssemble, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and discharges the universal claim by fin_cases on all six indices. Each chunk theorem such as this one supplies one ground instance those fin_cases land on.
In the broader Gravity stack this identity is part of certifying the exact midpoint M2TT kernel used in the Regge analysis. It is pure discrete bookkeeping: no continuum limit, no RS forcing-chain step (T0–T8), and no appeal to J-cost or the Recognition Composition Law. Its role is to keep the 256-case kernel proof modular and machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.