e_030010
plain-language theorem explainer
For the six-index slot (0,3,0,0,1,0) on Fin 4, the folded Regge midpoint numerator equals eight times the explicit closed-form kernel value. Gravity analysts cite it when assembling the full 4D M2 TT identity over all 4^6 index tuples. The proof is a single kernel decide on two concrete integers.
Claim. With $a,b,c,d,i,j\in\{0,1,2,3\}$, the midpoint numerator at $(0,3,0,0,1,0)$ satisfies $m_2^{\mathrm{num}}(0,3,0,0,1,0)=8\,Z_{\mathrm{expl}}(0,3,0,0,1,0)$, where $m_2^{\mathrm{num}}$ is the fold of coupling contributions and $Z_{\mathrm{expl}}$ is the explicit integer kernel.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple in $(\mathrm{Fin},4)^6$. The module doc states the goal as $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$, chunk 3, discharged by 256 kernel decides.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and summing each contribution at those indices. $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six Fin-4 arguments (sample values include $4$, $-2$, and so on for the listed patterns).
The local setting is pure finite enumeration: no continuum limit, no floating arithmetic. Each chunk theorem pins one concrete multi-index so the assembler can recombine them into a universal identity.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left via the fold definition of the numerator, the right via the pattern match on the explicit kernel (or zero if unmatched). Lean’s kernel checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the parent assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices. That universal equality is the certified algebraic core of the 4D Regge midpoint M2 TT identity in the Gravity analysis stack.
Within Recognition Science gravity work, such exact discrete identities underwrite curvature and mass-ladder bookkeeping on the phi-ladder side without residual numerical error. This declaration is one of the 256 atomic decides in chunk 3; it closes no open physics conjecture by itself, but removes one index cell from the residual of the full identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.