e_210311
plain-language theorem explainer
Concrete six-index case of the 4D Regge midpoint identity: the folded coupling numerator at (2,1,0,3,1,1) equals eight times the explicit Z-table entry. Gravity analysts cite it as one of 256 kernel decides that assemble the global m2Num = 8·explicitZ statement. The proof is a single kernel decide on fixed integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,3,1,1)$ with each coordinate in $\{0,1,2,3\}$, 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 9 of a 256-case kernel certification that the 4D Regge exact-midpoint mass-squared numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list: it accumulates integer weights for each multi-index. The companion table $\mathrm{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments (sample clauses return $4$, $-2$, etc.).
The local claim is one pointwise instance of $m_2^{\mathrm{num}}=8\cdot Z$ at the concrete tuple $(2,1,0,3,1,1)$. Sibling theorems cover the other tuples in the same chunk.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern table for $Z$. Lean’s decision procedure checks integer equality; no algebraic lemmas 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\cdot Z$ by exhausting all $\mathrm{Fin},4$ cases. That global identity is part of the Regge exact-midpoint M2/TT certification in the gravity analysis stack: it replaces a symbolic coupling sum by an explicit sparse integer kernel.
In the Recognition Science gravity line this is bookkeeping infrastructure, not a forcing-chain step (T0–T8). It underwrites exact discrete curvature/mass-squared identities used downstream when matching continuum limits and ladder normalizations. Open scaffolding is only the remaining unproved sibling index chunks, if any; this particular case is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.