e_213002
plain-language theorem explainer
For the six-index slot (2,1,3,0,0,2) on Fin 4, the folded Regge coupling numerator equals eight times the closed-form explicit Z value at that slot. Gravity analysts cite it when discharging one cell of the 4D midpoint M2 TT identity kernel. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(2,1,3,0,0,2)=8\,Z_{\mathrm{exp}}(2,1,3,0,0,2)$, where $Z_{\mathrm{exp}}$ is the explicit integer table and $m_2^{\mathrm{num}}$ is the fold of all coupling contributions at that multi-index.
background
This module is chunk 9 of a 256-cell kernel certification that the folded Regge midpoint numerator equals eight times an explicit integer table on every six-tuple in $(\mathrm{Fin},4)^6$. The ambient setting is the 4D Regge exact-midpoint M2 TT identity: discrete curvature couplings are reduced to integer arithmetic so the identity can be machine-checked.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing each contribution at the six indices. The companion table $Z_{\mathrm{exp}}$ is a pattern-matched integer function on the same six Fin 4 arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns). The claim here is one concrete cell of the equality $m_2^{\mathrm{num}}=8,Z_{\mathrm{exp}}$.
proof idea
One-line computational proof: by decide. Both sides evaluate to concrete Int values once the six Fin 4 arguments are fixed, so the kernel closes the equality without lemmas or rewriting. No algebraic identity is invoked at this cell; the work is pure evaluation of the fold versus the table.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{exp}}$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one decided cell so the assemble proof can finish without a monolithic kernel run. In the gravity stack this certifies the numerator side of the 4D Regge exact-midpoint M2 TT identity, a discrete consistency check on curvature couplings before continuum or continuum-limit claims. It is bookkeeping inside the Gravity analysis layer, not a forcing-chain (T0–T8) step, but it hardens the discrete geometric substrate those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.