e_210100
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,1,0,1,0,0) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D midpoint M2 numerator identity over (Fin 4)^6. Proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,0,1,0,0)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(2,1,0,1,0,0)=8\,Z_{\mathrm{expl}}(2,1,0,1,0,0)$.
background
This module is chunk 9 of a 256-case kernel certification that the 4D Regge midpoint M2 numerator matches a closed integer table. Indices run over $\mathrm{Fin},4$ (four discrete slots), matching the 4D simplex bookkeeping in the parent Gravity.Analysis development.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z_{\mathrm{expl}}$ is an explicit six-argument integer table on $(\mathrm{Fin},4)^6$, with sparse nonzero entries such as $Z_{\mathrm{expl}}(0,0,1,1,2,2)=4$ and $Z_{\mathrm{expl}}(0,0,1,2,1,2)=-2$.
The global claim is $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at every multi-index. Each chunk theorem pins one concrete tuple so the assembler can discharge the universal statement by exhaustive case split.
proof idea
One-line kernel proof: decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are literal numerals (here $2,1,0,1,0,0$). Lean reduces the fold that defines the numerator and the pattern-match that defines the explicit table, then checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ and $Z_{\mathrm{expl}}$.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ for all $a,b,c,d,i,j:\mathrm{Fin},4$, which is proved by nested fin_cases over the six indices and relies on these pointwise chunk certificates. That universal identity is the numerical heart of the Regge exact-midpoint M2 TT identity in 4D: it certifies that the folded coupling numerator is exactly eight times a sparse explicit integer kernel.
In the broader Recognition gravity stack this is bookkeeping infrastructure, not a forcing-chain step (T0–T8). It locks the discrete 4D midpoint calculus so later continuum or continuum-limit arguments can quote a fully discharged algebraic identity rather than an unchecked table. Sibling chunks cover the other multi-indices; this declaration is only the $(2,1,0,1,0,0)$ cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.