e_201130
plain-language theorem explainer
Pointwise identity: the midpoint M2 numerator at multi-index (2,0,1,1,3,0) equals eight times the explicit integer kernel Z at that index. Gravity analysts cite it when assembling the full Fin-4^6 identity for the 4D Regge midpoint M2 TT kernel. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,1,1,3,0)$ with each coordinate in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the M2 TT numerator is built by folding a fixed coupling list: each term contributes an integer contrib, and m2Num a b c d i j is their total. The companion table explicitZ is a closed-form integer kernel on $(\mathrm{Fin},4)^6$, with sparse nonzero entries such as $4$ on matched pairs and $-2$ on crossed pairs.
This module is chunk 8 of a 256-way case split that checks $m_2^{\mathrm{num}}=8\cdot Z$ at every multi-index. The local setting is pure integer arithmetic on finite indices; no continuum limit or metric signature is invoked here. Upstream, both sides are pure defs: the left is a fold, the right a pattern-matched constant table.
proof idea
One-line computational proof: decide evaluates both integer sides at the concrete six-tuple $(2,0,1,1,3,0)$ and confirms equality. No lemmas are invoked beyond the kernel definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by exhaustive fin_cases. That universal equality is the algebraic certificate that the midpoint M2 TT numerator is exactly eight copies of the explicit kernel, a step in the discrete gravity analysis chain. It does not itself touch continuum GR or the RS forcing landmarks (T5–T8); it is bookkeeping that makes the 4D kernel identity machine-checkable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.