e_102103
plain-language theorem explainer
For the Fin-4 multi-index (1,0,2,1,0,3), the M2 numerator equals eight times the explicit integer kernel Z. Gravity analysts checking the 4D Regge midpoint TT identity cite this as one concrete cell of the 256-case kernel grid. The proof is a single decide on the two integer sides.
Claim. At multi-index $(1,0,2,1,0,3)$ on $\mathrm{Fin}\,4$, the M2 numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(1,0,2,1,0,3)=8\,Z(1,0,2,1,0,3)$.
background
In the 4D Regge midpoint analysis, the M2 numerator is the fold of a fixed coupling-contribution list over six indices in $\mathrm{Fin},4$. The explicit kernel $Z$ is a piecewise integer table on those same indices (sample values $4$, $-2$, and so on). The local module certifies, cell by cell, that the folded numerator is exactly eight times this table.
This file is chunk 4 of the 256 kernel decides that exhaust the $\mathrm{Fin},4^6$ grid. Upstream, $m_2^{\mathrm{num}}$ is defined by folding couplingZList with a per-term contribution, while $Z$ is the closed integer case table used as the target closed form.
proof idea
One-line computational proof: decide evaluates both sides under the concrete indices to integers and checks equality. No algebraic rewrite lemmas are applied beyond unfolding the definitions of the numerator fold and the explicit kernel table.
why it matters
This cell feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ for all six $\mathrm{Fin},4$ arguments by exhaustive fin_cases. That identity is the algebraic backbone of the Regge exact midpoint M2 TT identity in the 4D gravity analysis stack. Closing every chunk discharges the numerator side of the kernel certificate used downstream in the TT-projection exactness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.