e_230031
plain-language theorem explainer
At multi-index (2,3,0,0,3,1) the folded coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel point checks that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,0,0,3,1)$ 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 chunk 11 of a 256-point kernel certification that the 4D Regge midpoint mass-squared numerator matches eight times an explicit integer table. Indices run over $\mathbb{F}_4$ (four values), so six indices give $4^6=4096$ formal slots; the certification partitions the nontrivial kernel into decide-sized chunks.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the given six-index slot. The comparison target explicitZ is a sparse pattern-matched integer table on the same six $\mathbb{F}_4$ arguments (typical nonzero entries are $\pm 2,\pm 4$).
Local goal of the chunk family: discharge $m_2^{\mathrm{num}}=8\cdot Z$ pointwise so a later assembly theorem can quantify over all indices by fin_cases.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values at the fixed indices $(2,3,0,0,3,1)$ (left via the fold definition of the numerator, right via the pattern table and the factor $8$), and the kernel equality checker closes the goal with no lemmas or rewriting.
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\cdot Z$ and proves it by exhaustive fin_cases on the six $\mathbb{F}_4$ indices, invoking one chunk equality per case. Without these point checks the global Regge midpoint M2/TT numerator identity in 4D cannot be closed inside Lean.
In the gravity analysis stack this is bookkeeping infrastructure for the exact discrete curvature/mass-squared coupling, not a new physical law. It sits downstream of the kernel certificate definitions and upstream of any theorem that quotes the assembled identity. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; the content is pure finite integer algebra on the Regge index set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.