e_013103
plain-language theorem explainer
For the six-index tuple (0,1,3,1,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2TT relation. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}3$, $d{=}1$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the integer $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding coupling contributions equals $8$ times the tabulated kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer via a local contribution map, and the fold starts at zero. The comparison target is an explicit piecewise table $Z$ that returns small integers (typically $\pm 2$ or $4$) on selected index patterns and is used as a closed form.
The module is one chunk of a 256-case kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is purely discrete: no continuum limit or metric signature is invoked here; only equality of two Int-valued functions on a finite domain.
proof idea
Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed. The tactic decide discharges the equality by computational reflection on those integers. No intermediate lemmas are invoked beyond the definitions of the fold numerator and the explicit table.
why it matters
This is one atomic case in the chunked proof that $m_2^{\mathrm{num}}=8Z$ for every six-tuple in $(\mathrm{Fin},4)^6$. The parent assembler m2Num_eq_eight_explicitZ introduces all six indices and splits by fin_cases, consuming these pointwise facts. That global identity is the algebraic backbone of the Regge-exact midpoint M2TT certification in the gravity analysis stack: it replaces a folded coupling sum by an eightfold multiple of a sparse explicit kernel, which is what later curvature and deficit identities need in closed form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.