e_331021
plain-language theorem explainer
For the concrete index sextuple (3,3,1,0,2,1) in (Fin 4)^6, the folded midpoint M2 numerator equals eight times the explicit integer Z-kernel. Gravity analysts assembling the 4D Regge exact-midpoint identity cite this as one of the 256 decided kernel cells. The proof is a single native decide on the two integer sides.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ for the fold of coupling contributions over the fixed coupling list, and $Z(a,b,c,d,i,j)$ for the explicit integer kernel table. Then $m_2^{\mathrm{num}}(3,3,1,0,2,1)=8\,Z(3,3,1,0,2,1)$.
background
This module is chunk 15 of a case-split campaign proving $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of indices in $\mathrm{Fin},4$. The ambient setting is the 4D Regge exact-midpoint $M_2$ TT-identity kernel certification: one must match a summed numerator built from discrete couplings against a sparse explicit integer table.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding contrib over couplingZList, starting from 0. The comparison table $Z$ is a pattern-matched function $\mathrm{Fin},4^6\to\mathbb{Z}$ that returns small integers (typically $\pm 2,\pm 4$, or 0 off the listed patterns).
Only the six concrete digits matter here: $(3,3,1,0,2,1)$. Sibling theorems in the same chunk discharge the neighboring cells; the full universal statement is assembled downstream by exhausting all $\mathrm{Fin},4$ cases.
proof idea
Both sides evaluate to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed. The proof is the single tactic decide, which reduces the equality of those integers in the kernel and closes the goal with no further lemmas. No algebraic rewriting or induction is required; the work is pure ground computation of the fold versus the pattern table.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts the identity for every sextuple $(a,b,c,d,i,j)$ in $(\mathrm{Fin},4)^6$. Its proof introduces the six variables and runs fin_cases on each; the residual ground goals are exactly the chunk theorems such as this one.
In the Recognition gravity stack, that universal equality is the certified bridge between the folded coupling numerator and the explicit $Z$ kernel used in the 4D Regge exact-midpoint $M_2$ TT identity. Closing the 256 decided cells removes a scaffolding obligation on the discrete curvature side of the analysis. The result is local to the integer kernel bookkeeping; it does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the $\varphi$-ladder mass formula, but it is part of the gravity-analysis substrate those layers sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.