e_200311
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,0,0,3,1,1) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one of the 256 kernel decides that assemble the global m2Num = 8·explicitZ statement. Proof is a single native decide on concrete Fin-4 integers.
Claim. At the multi-index $(a,b,c,d,i,j)=(2,0,0,3,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer table entry: $N(2,0,0,3,1,1)=8\,Z(2,0,0,3,1,1)$.
background
This module is chunk 8 of a 256-way kernel split proving the numerator identity $N=8Z$ for the 4D Regge exact-midpoint TT sector. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry for the six indices. The closed form $Z=\mathrm{explicitZ}$ is an explicit integer-valued table on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local claim is one concrete sextuple inside that table comparison. Upstream, both $N$ and $Z$ live in the kernel-cert module that supplies the shared definitions used by every chunk.
proof idea
One-line computational proof: decide. After substituting the concrete Fin-4 literals $(2,0,0,3,1,1)$, both sides reduce to closed integers (the fold for $N$ and the match for $Z$), and the kernel decides equality to $8Z$ with no further lemmas.
why it matters
Feeds the assembly theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the quantifiers by exhaustive $\mathrm{fin_cases}$ on all six indices. Each chunk theorem such as this one covers one residue class of that case split (module doc: "m2Num = 8·explicitZ, chunk 8 (256 kernel decides)").
In the gravity stack this identity is bookkeeping for the exact-midpoint Regge TT kernel in 4D: once $N=8Z$ is global, downstream curvature and continuum-limit arguments can replace the folded coupling by the cheap explicit table. It is infrastructure inside the Gravity domain, not a T0–T8 forcing step, but it hardens the discrete-to-continuum bridge used by RS gravitational claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.