e_210232
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at Fin-4 indices (2,1,0,2,3,2) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one kernel cell in the 4D Regge midpoint M2 TT identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,2,3,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(2,1,0,2,3,2)=8\,Z_{\mathrm{expl}}(2,1,0,2,3,2)$.
background
This module is chunk 9 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator agrees with an explicit closed form: $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on every sextuple of $\mathrm{Fin},4$ indices.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of couplingZList, summing a local contribution at each coupling term. $Z_{\mathrm{expl}}$ is a hand-written integer table on six $\mathrm{Fin},4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). Both live in the kernel certificate module.
The present declaration fixes one concrete cell of that table comparison.
proof idea
One-line computational proof: decide evaluates both sides at the literal indices $(2,1,0,2,3,2)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of the numerator fold and the explicit table.
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,Z_{\mathrm{expl}}$ and discharges the universal quantifier by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk cell such as this one supplies a decided ground instance the case split can close.
In the Recognition gravity stack this is bookkeeping for the 4D Regge midpoint M2 TT identity: once every kernel cell matches, the numerator is interchangeable with the explicit form in later curvature and mass-gap arguments. It does not itself touch T0–T8 or the RCL; it is pure discrete tensor algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.