e_020010
plain-language theorem explainer
At multi-index (0,2,0,0,1,0), the folded Regge numerator equals eight times the explicit kernel table entry. Gravity analysts cite it as one point check in the 256-way split of the 4D midpoint M2TT identity. Proof is a single kernel decide on concrete integers.
Claim. The folded integer numerator $m_2^{\mathrm{num}}(0,2,0,0,1,0)$ equals $8$ times the explicit table value $Z(0,2,0,0,1,0)$ on six indices in $\{0,1,2,3\}$.
background
In the 4D Regge exact-midpoint gravity analysis, two integer kernels on six indices drawn from $\mathrm{Fin},4$ are compared pointwise. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each term's contribution at the given multi-index. The companion map $Z$ is an explicit sparse table of small integers (entries such as $4$, $-2$, and so on) obtained by pattern match on the six indices.
This module is chunk 2 of a 256-way case split whose sole job is to certify $m_2^{\mathrm{num}}=8\cdot Z$ at every sextuple. The local setting is pure finite enumeration: no continuum limit, no physical units, only integer equality after folding versus table lookup.
proof idea
One-line wrapper: both sides are closed integer terms at a fixed multi-index, so decide evaluates them in the kernel and closes the equality. No lemmas beyond the definitions of the folded numerator and the explicit table are required.
why it matters
Feeds the assembly theorem that states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$. That parent exhausts all $\mathrm{Fin},4$ sextuples by nested fin_cases and dispatches each cell to a chunk lemma of this form. The identity is a certification step inside the Regge midpoint M2TT kernel stack for 4D gravity, not a continuum or observational claim. It sits downstream of the coupling-list and table definitions and upstream of the full pointwise equality used by later gravity-analysis certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.