e_333301
plain-language theorem explainer
For the single multi-index (3,3,3,3,0,1) on Fin 4, the summed coupling numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one atomic cell in the exhaustive 4^6 case split that builds the global identity. The proof is a pure kernel decide on integer equality.
Claim. With $a=b=c=d=3$, $i=0$, $j=1$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(3,3,3,3,0,1)=8\,Z_{\mathrm{ex}}(3,3,3,3,0,1)$.
background
In the Regge midpoint 4D analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator m2Num folds a fixed coupling list, accumulating each term's contribution at the given indices. The companion explicitZ is a sparse pattern-matched table of small integers (entries such as 4, -2, ...) that is meant to be the closed form of that sum, up to a universal factor of 8.
This module is chunk 15 of the decide-driven verification that the two kernels agree after that factor. The local setting is pure finite enumeration: no continuum limit, no curvature hypothesis, only integer arithmetic on a 4^6 grid of index tuples.
proof idea
One-line decide. Lean reduces both sides of the integer equality for the concrete tuple (3,3,3,3,0,1) and checks they match. No lemmas are invoked beyond the definitions of m2Num (fold of contrib over couplingZList) and explicitZ (pattern table).
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by nested fin_cases and discharges each leaf with a chunk theorem of this form. Establishing m2Num = 8·explicitZ is the algebraic backbone of the Regge-exact midpoint M2/TT identity in 4D: once the numerator is replaced by the sparse explicit table, later gravity certificates can reason symbolically instead of re-folding the coupling list. The factor 8 is bookkeeping from the discrete midpoint stencil, not a continuum curvature claim. No Recognition forcing step (T0–T8) is touched here; the result is pure discrete GR kernel hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.