e_201311
plain-language theorem explainer
At multi-index (2,0,1,3,1,1) the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of 256 concrete kernel checks that assemble into the global identity. The proof is a single native decide on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,3,1,1)$ with each entry in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-point kernel certification that the midpoint Regge $m_2$ numerator equals eight times an explicit integer table on $(\mathbb{F}_4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on).
The local claim is the equality at one concrete six-tuple. Upstream supplies only those two definitions; no analytic lemma is required beyond evaluation.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted into m2Num and explicitZ, so the kernel decision procedure closes the equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathbb{F}_4)^6$ and discharges it by exhaustive fin_cases. Each chunk such as this one pins a single point of that $4^6=4096$-case (here organized as 256 kernel decides) grid.
In the gravity analysis stack this identity is bookkeeping for the exact midpoint Regge $m_2$ tensor structure in 4D: the folded coupling sum is replaced by a closed-form integer kernel times eight. It is infrastructure inside the RS gravity pipeline, not a forcing-chain (T0–T8) step, but it keeps the discrete curvature numerics exact rather than approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.