e_020113
plain-language theorem explainer
At multi-index (0,2,0,1,1,3) the folded Regge coupling numerator equals eight times the explicit Z-table entry. Gravity analysts assembling the 4D midpoint M2 TT identity cite this as one concrete kernel point among the 256 Fin-4 cases. The proof is a single decide on fully concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,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 table value $Z(a,b,c,d,i,j)$.
background
This module sits in the Gravity analysis stack that certifies an exact midpoint identity for the Regge M2 TT kernel in 4D. The local goal, stated in the module header, is to check $m_2^{\mathrm{num}}=8\cdot Z$ on chunk 2 of the 256-point Fin-4 grid by kernel decides.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer weight at the six indices, and the fold starts from 0. The comparison table $Z$ is an explicit six-index integer function on $\mathrm{Fin},4$, with sparse nonzero cases such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$.
Both objects live in the KernelCert module; this chunk only evaluates them at one fixed tuple.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel closes the equality with no lemmas and no case split inside this declaration.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ by exhausting all six Fin 4 indices. This declaration is the single grid point $(0,2,0,1,1,3)$ in that exhaustion (chunk 2 of the 256 decides).
In the broader RS gravity stack, the identity underwrites the exact midpoint evaluation of the Regge M2 TT kernel used in discrete curvature bookkeeping. It is pure integer algebra on a finite index set, not a continuum GR derivation, and it does not itself invoke the T0–T8 forcing chain or the J-cost RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.