e_311103
plain-language theorem explainer
Pointwise check that the folded Regge coupling numerator at multi-index (3,1,1,1,0,3) equals eight times the explicit integer table at those same indices. Gravity analysts cite it as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,1,1,0,3)$ in $(\mathrm{Fin}\,4)^6$, 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
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the given indices. The comparison target is an explicit piecewise table $Z$ on the same six indices, with small integer values such as $4$, $-2$, and so on at the matched patterns.
The local module is chunk 13 of a 256-cell kernel certification whose sole job is to discharge $m_2^{\mathrm{num}}=8\cdot Z$ at concrete index tuples by decision procedure. The ambient claim is the pointwise identity of those two kernels on all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: decide. Both sides evaluate to concrete integers once the six Fin-4 arguments are fixed, so the kernel decision procedure closes the equality with no lemmas and no case splits inside this declaration.
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$ and proves it by exhaustive fin_cases on the six indices. Each chunk cell such as this one supplies one of the 256 ground equalities the assembly relies on. In the broader gravity stack this certifies that the folded Regge midpoint numerator agrees with the closed-form integer table, a prerequisite for exact midpoint identities in the 4D TT sector. It is pure kernel bookkeeping, not a forcing-chain step (T0–T8), but it locks a numerical identity used downstream in the Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.