e_232113
plain-language theorem explainer
At multi-index (2,3,2,1,1,3) the folded Regge midpoint numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one atomic case in the 256-way exhaustion that m2Num = 8·explicitZ on (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,1,1,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 kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-case kernel certification that the Regge exact-midpoint mass-squared numerator matches eight times a closed-form integer table on four-valued indices.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the six indices. The table explicitZ is a pattern-matched integer function on $(\mathbb{F}_4)^6$ (sample values include $4$, $-2$, and other small integers on diagonal and off-diagonal patterns).
The local claim is purely combinatorial: one concrete six-tuple must satisfy the scalar identity before the global fin_cases assembly can conclude equality everywhere.
proof idea
One-line proof by decide. Lean evaluates both sides as concrete Int values (the fold of m2Num at $(2,3,2,1,1,3)$ versus $8$ times the matching explicitZ clause) and discharges the equality by kernel computation. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by six nested fin_cases over $\mathbb{F}_4$. Each chunk theorem such as this one is a leaf of that exhaustion (256 decides total).
In the gravity analysis stack this identity is the algebraic certificate that the midpoint Regge TT kernel is exactly eight times the tabulated $Z$ coupling, so later curvature and mass-ladder arguments can quote the closed form instead of the fold. It is bookkeeping inside the 4D kernel cert, not a new physical law; its value is that the case split is machine-checked rather than hand-waved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.