m2Num_eq_eight_explicitZ
plain-language theorem explainer
For every 6-tuple of indices in Fin 4, the integer numerator m2Num equals eight times the explicit kernel table entry explicitZ. Gravity analysts cite it when collapsing the folded coupling sum to a closed coefficient table. The proof is exhaustive fin_cases over all 4096 tuples, each goal closed by a precomputed decide lemma from the chunk modules.
Claim. For all indices $a,b,c,d,i,j \in \{0,1,2,3\}$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2 TT identity. The local goal, stated in the module doc, is to assemble the pointwise identity $m_2^{\mathrm{num}} = 8\cdot Z$ over every index 6-tuple in $\mathrm{Fin},4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined as a left fold of coupling contributions: it sums $\mathrm{contrib},t,a,b,c,d,i,j$ over the fixed list couplingZList, starting from 0. The comparison object $Z$ is an explicit integer lookup on six $\mathrm{Fin},4$ arguments (sample clauses: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$, and so on).
Because both sides are pure integer functions of a finite discrete domain of size $4^6=4096$, the identity is a finite verification problem. The work is split across chunk modules (Chunk00 through Chunk10 and beyond), each exporting named pointwise lemmas such as $m_2^{\mathrm{num}}(0,0,0,0,0,0)=8,Z(0,0,0,0,0,0)$ proved by decide.
proof idea
Introduce the six indices, then run nested fin_cases on $a,b,c,d,i,j$ in that order. Each of the 4096 residual goals is closed by exact against the matching precomputed chunk lemma (M2NumChunk00.e_000000, e_000001, ..., and the analogous exports from later chunks). Those chunk lemmas are themselves one-line decide proofs of the same equality at a fixed tuple. No algebraic rewriting of the fold occurs at this layer; the assembly is pure case dispatch onto certified point evaluations.
why it matters
The identity is the bridge from the folded coupling definition of the M2 numerator to the closed explicit $Z$ table used in kernel certification. Downstream, m2CoeffSum_eq_explicitM2CoeffZ rewrites with this theorem (together with the division relation $m_2^{\mathrm{coeffSum}}=m_2^{\mathrm{num}}/\ldots$ and the definition of the scale-32 table) to conclude that the coefficient sum equals the explicit M2 coefficient table for every index tuple.
In the broader gravity stack this is bookkeeping infrastructure for the Regge midpoint M2 TT identity in 4D: once numerators match $8Z$, coefficient normalizations become table lookups rather than live folds. It does not itself invoke the Recognition forcing chain (T5–T8) or the RCL; it is a discrete algebraic certificate inside the gravity analysis layer that those continuum claims later rely on for exact coefficient control.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.