e_200220
plain-language theorem explainer
At multi-index (2,0,0,2,2,0) on Fin 4, the folded Regge midpoint coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel point checks that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,2,2,0)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-way case split proving that the 4D Regge midpoint $m_2$ numerator coincides with eight times a closed-form integer table. The ambient setting is exact algebraic certification of a midpoint TT identity used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six Fin-4 indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
Each chunk theorem fixes one concrete six-tuple and asserts equality after multiplying the table entry by $8$. The present declaration is the case $(2,0,0,2,2,0)$.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of $m_2^{\mathrm{num}}$ and the pattern table for $\mathrm{explicitZ}$, so decidable equality on $\mathbb{Z}$ closes the goal with no further lemmas.
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\cdot Z$ and discharges the universal claim by exhaustive fin_cases over all six Fin-4 coordinates, invoking one chunk equality per cell. Without the full 256-point cover, the midpoint TT numerator identity remains uncertified.
In the Recognition gravity stack this is pure algebraic bookkeeping for the Regge midpoint sector in $D=3+1$, not a forcing-chain step (T5–T8). It closes a scaffolding obligation: every kernel cell must match before the assembled identity can be used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.