e_202003
plain-language theorem explainer
For the six-index slot (2,0,2,0,0,3) on Fin 4, the folded Regge numerator coupling equals eight times the explicit integer kernel entry. Gravity analysts certifying the 4D midpoint M2TT identity cite this as one atomic kernel check. The proof is a single `decide` on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the numerator coupling at $(a,b,c,d,i,j)=(2,0,2,0,0,3)$ satisfies $m_2^{\mathrm{num}}(2,0,2,0,0,3)=8\,Z(2,0,2,0,0,3)$, where $Z$ is the explicit integer kernel table.
background
This module sits in the Gravity analysis stack that certifies an exact algebraic identity for the midpoint Regge M2TT coupling in four dimensions. The local claim of the file is that the folded numerator equals eight times an explicit integer kernel, discharged in 256 small decide chunks.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution at each multi-index. The comparison table $Z$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a large pattern-match of constant integers (typical nonzero values $\pm2,\pm4$). Both live in the kernel-cert module imported here.
Indices run over $\mathrm{Fin},4$, matching a 4D discrete simplex/edge labeling. The factor 8 is the global normalization relating the folded sum to the closed-form kernel entry.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete six-tuple $(2,0,2,0,0,3)$ in the integer ring and checks equality. No lemmas are invoked beyond the reducible definitions of the folded numerator and the explicit kernel table.
why it matters
This is one cell in the exhaustive grid that builds m2Num_eq_eight_explicitZ, the parent theorem stating $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$. That assembler runs nested fin_cases over all six $\mathrm{Fin},4$ indices; each chunk such as this one supplies a pre-checked equality the kernel can reuse or that documents the 256-way split.
In the broader Recognition gravity line, the identity is bookkeeping for the exact midpoint Regge coupling in $D=4$, not a derivation of $D=3$ from the forcing chain. It closes a pure algebraic certification step so later continuum or continuum-limit arguments can treat the numerator/kernel relation as settled integer arithmetic rather than an open summation identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.