e_021202
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at index sextuple (0,2,1,2,0,2) equals eight times the tabulated explicit integer. Gravity analysts assembling the full Regge midpoint M2TT identity cite this as one of 256 kernel cells. The proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,2,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling sum $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certifying that the Regge exact-midpoint numerator equals eight times a tabulated integer form, pointwise on all sextuples in $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it accumulates every contribution term at the six indices and returns an integer. The comparison target $Z$ is an explicit pattern-matched table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for the listed patterns).
The local goal is purely arithmetic: evaluate both sides at one fixed sextuple and check equality of integers. No continuum limit or variational argument is involved at this layer.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list on the left; the pattern table on the right), so the equality is a decidable integer identity 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}}=8Z$ and discharges the universal claim by exhaustive fin_cases over all six indices, invoking one cell theorem per sextuple.
In the gravity analysis stack this identity is bookkeeping for the exact midpoint form of the 4D Regge M2TT kernel: once every cell matches, the closed form $Z$ may replace the folded sum in downstream curvature or mass-gap arguments. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure inside the discrete gravity certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.