e_010310
plain-language theorem explainer
For the six-index slot (0,1,0,3,1,0) on Fin 4, the folded numerator m2Num equals eight times the tabulated kernel value explicitZ. Gravity analysts cite it when assembling the global identity m2Num = 8·explicitZ over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,3,1,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,1,0,3,1,0)=8\,Z_{\mathrm{explicit}}(0,1,0,3,1,0)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT-identity certification. The numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an integer for each six-tuple of Fin 4 indices.
The comparison target explicitZ is a closed-form integer table on the same six Fin 4 arguments (sample clauses include values 4, -2, and so on for distinguished index patterns). The local claim of the chunk family is the pointwise identity m2Num = 8 · explicitZ.
Chunk 1 discharges 256 concrete kernel instances by decide. The present declaration is the instance at indices (0,1,0,3,1,0).
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left via the fold definition of m2Num, the right via the pattern-match table explicitZ scaled by 8. The kernel checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple of Fin 4 indices and proves it by exhaustive fin_cases on each coordinate, landing on chunk lemmas such as this one. That global equality is the certified numerator half of the Regge exact-midpoint M2 TT identity in 4D gravity analysis inside the monolith. It does not itself touch the T0–T8 forcing chain or the J-cost; it is pure discrete kernel bookkeeping supporting the continuum gravity side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.