e_212103
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,1,2,1,0,3) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel cells assembling the global m2Num = 8·explicitZ theorem. Proof is a single kernel decide on concrete Int values.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,2,1,0,3)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the closed-form table: $m_2^{\mathrm{num}}(2,1,2,1,0,3)=8\,Z_{\mathrm{explicit}}(2,1,2,1,0,3)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{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 contribution term at the given multi-index. The companion $Z_{\mathrm{explicit}}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The local module is chunk 9 of a 256-cell kernel certification that $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ holds at every sextuple. Each chunk theorem pins one concrete cell so the assembly proof can discharge the universal quantifier by exhaustive fin_cases.
Upstream, only the two definitions are needed: the fold that builds the numerator and the explicit table that supplies the closed form.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values at the fixed indices $(2,1,2,1,0,3)$, so the equality is a decidable integer comparison with no lemmas or rewriting beyond evaluation of m2Num and explicitZ.
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{explicit}}$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, invoking one cell theorem per sextuple. Without the full 256-cell cover, the global midpoint TT-identity numerator reduction stays open.
In the gravity stack this is bookkeeping infrastructure for the Regge exact-midpoint $M_2$ identity in 4D, not a forcing-chain landmark (T5–T8). It closes a finite computational obligation so higher geometric claims can treat the factor-of-eight relation as proved rather than tabulated by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.