e_210210
plain-language theorem explainer
For the six-index slot (2,1,0,2,1,0) on Fin 4, the folded Regge midpoint numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one atomic cell of the 4D midpoint M2TT identity. The proof is a single decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,2,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8\,Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer kernels on six Fin-4 indices are compared. The numerator m2Num is the fold of a fixed coupling list: it sums a local contribution at each coupling triple against the six free indices. The comparison target explicitZ is a sparse closed-form table on the same six indices (nonzero only on a short list of patterns such as (0,0,1,1,2,2)mapsto 4 and (0,0,1,2,1,2)mapsto -2).
The module is chunk 9 of a 256-cell decide grid that exhausts the identity m2Num = 8 · explicitZ pointwise. The local setting is pure integer kernel certification: no continuum limit, no physical units, only the discrete midpoint stencil.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are fixed at (2,1,0,2,1,0), so the decision procedure discharges the equality with no lemmas beyond the definitions of m2Num and explicitZ.
why it matters
This cell is consumed by m2Num_eq_eight_explicitZ, which states the universal identity for all six Fin-4 indices and proves it by nested fin_cases. Each concrete goal in that case split is exactly one chunk theorem of this form. Closing the pointwise grid certifies that the folded midpoint numerator is identically eight times the explicit kernel, a discrete algebraic step inside the 4D Regge M2TT identity used in the gravity analysis stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.