e_313103
plain-language theorem explainer
For the single six-index slot (3,1,3,1,0,3) on Fin 4, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it only as one of the 256 concrete cases feeding the global m2Num = 8·Z identity. The proof is a pure kernel decision on two closed integer expressions.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,1,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local claim is the pointwise equality $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index space, discharged by kernel decides rather than by algebraic rewriting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six Fin-4 indices. The comparison object $Z$ is an explicit integer-valued table on the same six indices (sample entries include $4$, $-2$, and so on for the listed patterns).
Upstream, both objects live in the kernel-certificate module; this chunk only evaluates them at one concrete tuple.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int values (the fold that defines the numerator, and the table lookup that defines $Z$) and checks equality. No lemmas are invoked; the tactic closes because both expressions are definitionally computable at this fixed index tuple.
why it matters
Parent theorem is the assembled identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$, proved by exhaustive fin_cases over all six Fin-4 arguments. Each chunk theorem such as this one supplies one (or a block of) decided cases that the assembler relies on.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT kernel in 4D: it certifies that the folded coupling numerator is exactly eight copies of the closed-form integer kernel, so later curvature and mass-ladder arguments can quote the compact $Z$ table instead of the fold. It does not itself touch T5–T8 or the RCL; it is infrastructure inside the gravity-analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.