e_221013
plain-language theorem explainer
For the concrete Fin-4 indices (2,2,1,0,1,3), the folded midpoint numerator equals eight times the explicit kernel integer. Gravity analysts building the Regge exact midpoint M2TT identity cite this as one atomic kernel check among the chunked decides. Proof is a single computational `decide` on closed integer arithmetic.
Claim. For indices $a=2$, $b=2$, $c=1$, $d=0$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the folded numerator equals eight times an explicit sparse kernel on every sextuple of Fin-4 indices. The module header states the local goal as "$m_2^{\mathrm{num}} = 8\cdot Z$, chunk 10 (256 kernel decides)."
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution at each term. The explicit kernel $Z$ is a pattern-matched integer table on six Fin-4 arguments (typical nonzero values $\pm 2,4$ on a sparse support). Both live in the kernel-certificate module imported here.
The ambient setting is discrete gravity analysis: verifying an exact algebraic identity for the midpoint M2TT operator in four dimensions by exhaustive evaluation on the finite index cube, rather than by symbolic cancellation alone.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin-4 literals are substituted into the fold definition of the numerator and the pattern match for the explicit kernel. Lean’s decision procedure closes the resulting integer equality with no lemmas or rewriting.
why it matters
This is one atomic cell in the exhaustive cover that assembles the global identity
$\forall a,b,c,d,i,j:; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$.
The parent theorem m2Num_eq_eight_explicitZ introduces all six indices and runs nested fin_cases; each residual goal is discharged by a chunk theorem of this form.
In the Recognition gravity stack, that global equality is the certified numerator half of the Regge exact-midpoint M2TT identity in 4D. Without the pointwise checks, the assemble step cannot finish. The result is pure finite verification: no continuum limit, no continuum curvature claim, and no link yet to the T8 $D=3$ forcing or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.