e_313313
plain-language theorem explainer
For the Fin-4 index sextuple (3,1,3,3,1,3), the folded midpoint numerator equals eight times the explicit kernel integer. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this cell among the 256 kernel cases. Proof is a single kernel decide on the concrete integers.
Claim. For indices $a=3$, $b=1$, $c=3$, $d=3$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the tabulated explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times an explicit integer table. Indices run over Fin 4, i.e. coordinate labels ${0,1,2,3}$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function on six Fin 4 arguments, given by a finite pattern table of small integers (entries such as $4$, $-2$, and so on).
The local claim is one concrete cell of that table identity: the fold at $(3,1,3,3,1,3)$ matches $8\cdot Z$ at the same point.
proof idea
One-line kernel proof: by decide. Both sides reduce to closed integer expressions (the fold over the fixed coupling list versus eight times the matching explicitZ clause), so the decision procedure discharges equality with no further lemmas.
why it matters
Parent theorem m2Num_eq_eight_explicitZ quantifies over all six Fin 4 indices and proves $m_2^{\mathrm{num}}=8Z$ everywhere by exhaustive fin_cases. Each chunk theorem such as this one supplies one concrete cell so the assemble proof can close without recomputing the fold.
In the gravity analysis stack this identity is the algebraic backbone of the exact midpoint M2TT relation in 4D Regge calculus. It is bookkeeping, not a new physical law, but the certified table is what lets later curvature and mass-ladder arguments treat the midpoint kernel as an explicit integer rather than a symbolic sum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.