e_312303
plain-language theorem explainer
For the single multi-index (3,1,2,3,0,3) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D midpoint M2TT identity case-by-case. The proof is a pure kernel decide on that fixed tuple.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer kernel, one has $N(3,1,2,3,0,3)=8\,Z(3,1,2,3,0,3)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add each list entry's contribution at the given indices. The comparison target $Z=\mathrm{explicitZ}$ is a closed-form piecewise integer table on the same six indices (typical nonzero values $\pm 2,,4$ on matched pairs).
This module is chunk 13 of a 256-way kernel split whose sole job is to discharge $N=8Z$ on concrete index tuples. The local setting is pure finite enumeration: no continuum limit and no floating-point arithmetic, only exact Int equalities on Fin 4.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(3,1,2,3,0,3)$ and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel table.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts $N=8Z$ for every six-tuple in $(\mathrm{Fin},4)^6$, proved by exhaustive fin_cases. This declaration is one concrete cell in that case tree (chunk 13 of the 256 kernel decides). It is bookkeeping infrastructure for the Regge midpoint M2TT identity in 4D gravity, not a forcing-chain (T0–T8) step; it simply certifies that the folded coupling numerator matches the explicit kernel on this index.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.