e_010030
plain-language theorem explainer
Kernel certificate for one multi-index: the Regge midpoint m2 numerator at (0,1,0,0,3,0) equals eight times the explicit Z table value. Gravity analysts cite it when assembling the full m2Num = 8·explicitZ identity over Fin 4^6. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,0,3,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of the 256 kernel decides that certify $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on $(\mathrm{Fin},4)^6$ in the 4D Regge exact-midpoint TT-identity analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six indices. The comparison table $Z$ is an explicit pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (nonzero only on a sparse set of index patterns, with values such as $\pm 2,\pm 4$).
The local claim is the single lattice point $(0,1,0,0,3,0)$. Sibling theorems cover the other points in the same chunk; the assemble theorem quantifies over all indices.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold for $m_2^{\mathrm{num}}$ and the pattern match for $Z$), so the equality is discharged by the kernel decision procedure with no lemmas or rewriting.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by exhausting $\mathrm{Fin},4$ on each coordinate. That global identity is the certified bridge between the folded coupling definition and the closed-form Z table in the Regge midpoint M2/TT analysis.
In the Recognition gravity stack this is pure discrete bookkeeping: it locks one lattice cell of the 4D kernel so the continuum or continuum-limit arguments can quote a fully decided algebraic identity rather than an open summation. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is infrastructure under the Regge exact-midpoint certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.