e_021311
plain-language theorem explainer
For the six-index slot (0,2,1,3,1,1) on the 4D midpoint kernel, the folded numerator m2Num equals eight times the closed-form table explicitZ. Gravity analysts assembling the exact Regge midpoint M2 identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,3,1,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching the four spacetime directions in the discrete midpoint calculus.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The table $\mathrm{explicitZ}$ is a pattern-matched integer function on six $\mathrm{Fin},4$ arguments (typical nonzero values $\pm 2,\pm 4$ on paired index patterns).
The local claim is one concrete six-tuple equality inside that kernel grid. Downstream assembly will quantify over all $4^6$ slots by case-splitting on each coordinate.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int values. The left side runs the fold that defines $m_2^{\mathrm{num}}$ on the fixed indices $(0,2,1,3,1,1)$; the right side looks up $8\cdot\mathrm{explicitZ}$ at the same slot. No lemmas are invoked beyond decidable equality of integers.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases over the six indices. Each chunk cell such as this one discharges one branch of that case tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $M_2$ kernel in 4D: once every cell matches, the folded coupling form collapses to the sparse closed table, simplifying later continuum or continuum-limit comparisons. It is pure discrete linear algebra on the kernel, not a derivation of $G$ or the $\phi$-ladder mass formula, but it is required scaffolding for trustworthy 4D Regge identities in the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.