e_232003
plain-language theorem explainer
For the six-index slot (2,3,2,0,0,3) on Fin 4, the folded Regge coupling numerator equals eight times the explicit kernel integer. Gravity analysts cite it when assembling the full midpoint M2 identity over the 4D index cube. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,0,0,3)$ in $\{0,1,2,3\}^6$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 256-case kernel certification that the midpoint Regge numerator matches eight times an explicit integer table on every 4D multi-index. The ambient setting is discrete gravity analysis: couplings are summed over a fixed list and compared to a closed-form kernel.
The numerator $N$ is defined by folding a contribution function over couplingZList, starting from 0. The explicit kernel $Z$ is a piecewise map $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$ on matched pairs such as $(0,0,1,1,2,2)$, $-2$ on crossed pairs). Both live in the kernel-cert module imported here.
Chunk 11 isolates a block of those index tuples so each equality can be discharged by a decidable integer computation rather than a symbolic expansion of the fold.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed: the fold that defines the numerator evaluates fully, the piecewise kernel returns a fixed Int, and Lean checks $N=8Z$ by computation. No lemmas beyond the definitions of the numerator and the explicit kernel are required.
why it matters
Parent assembly theorem m2Num_eq_eight_explicitZ states the identity for every $(a,b,c,d,i,j)$ in $\mathrm{Fin},4$, proved by exhaustive fin_cases. This declaration is one concrete cell in that cube (chunk 11), so the global midpoint M2 numerator identity is only as strong as these per-slot decides.
In the Recognition gravity stack, the exact midpoint identity is bookkeeping infrastructure for discrete curvature and coupling normalizations on the eight-tick / 4D lattice side. It does not itself invoke the J-cost or the forcing chain (T5–T8), but it underwrites numerical trust in the Regge-sector algebra those layers sit on.
Siblings in the same chunk cover the neighboring index patterns; together they close the 256-kernel decide plan named in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.