e_202002
plain-language theorem explainer
Pointwise identity: at multi-index (2,0,2,0,0,2) the folded Regge midpoint m₂ numerator equals eight times the explicit integer Z table. Gravity analysts cite it when assembling the full Fin-4⁶ certificate that m₂Num = 8·Z. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,2,0,0,2)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-way kernel split certifying the algebraic identity $m_2^{\mathrm{num}}=8\cdot Z$ on all six-tuples of $\mathrm{Fin},4$ indices arising in the 4D Regge midpoint $M_2$ TT analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison table $Z$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample values include $4$, $-2$, and $0$ on unmatched patterns).
The local claim is one concrete cell of that table identity, needed before the assembler can discharge the universal quantifier over all index sextuples.
proof idea
One-line computational proof: decide. Both sides reduce to closed integer expressions once the six $\mathrm{Fin},4$ arguments are substituted, so the kernel equality checker finishes without lemmas or rewriting.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on the six indices. Each chunk such as this one supplies a decided cell so the universal identity is not a single monolithic decide.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ TT kernel in 4D: it locks the folded coupling numerator to a sparse explicit integer table, a prerequisite for later continuum or continuum-limit comparisons. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure discrete tensor algebra supporting the gravity side of the mirror.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.