e_211333
plain-language theorem explainer
For the single multi-index (2,1,1,3,3,3), the folded numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a pure `decide` on the concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(2,1,1,3,3,3)=8\,Z_{\mathrm{explicit}}(2,1,1,3,3,3)$.
background
In the 4D Regge midpoint analysis, the M2–TT identity is checked by comparing a folded numerator against a closed-form integer kernel. The numerator m2Num is defined by folding contrib over couplingZList at a sextuple of Fin 4 indices. The comparison target explicitZ is a piecewise integer table on the same sextuples (sample clauses include value 4 on (0,0,1,1,2,2) and −2 on several mixed pairs).
This module is chunk 9 of the 256-cell kernel certification: each cell asserts m2Num = 8 · explicitZ at one concrete multi-index. The local setting is pure integer arithmetic on a finite index set, not continuum GR.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the fixed indices (2,1,1,3,3,3) and checks integer equality. No lemmas beyond the definitions of m2Num and explicitZ are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 and is proved by nested fin_cases that discharge each cell (including this one). That global equality is the algebraic core of the Regge-exact midpoint M2–TT identity certificate in 4D gravity analysis. It is bookkeeping inside the discrete curvature/coupling expansion, not a continuum Einstein-equation derivation, and does not itself invoke the RS forcing chain (T5–T8) or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.