e_310202
plain-language theorem explainer
For the multi-index (3,1,0,2,0,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a single kernel decide on two concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer kernel table, one has $N(3,1,0,2,0,2)=8\,Z(3,1,0,2,0,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on sextuples of Fin 4 indices are compared. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The companion map $Z=\mathrm{explicitZ}$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on).
The module is chunk 13 of a 256-cell kernel certification that $N=8Z$ pointwise. Each cell is an independent equality of two concrete integers; the present declaration is the cell at indices $(3,1,0,2,0,2)$. Upstream, only the definitions of $N$ and $Z$ are required.
proof idea
One-line proof by decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are substituted: the left-hand side evaluates the fold that defines the numerator, the right-hand side multiplies the table entry by eight. Lean’s kernel decision procedure discharges the resulting numeral equality.
why it matters
Parent theorem is the assembled identity $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$, proved by exhaustive fin_cases over all six indices and dispatch to the matching cell. This cell is one of those leaves. In the broader gravity stack it supports the exact midpoint M2TT identity used in the Regge analysis; it is pure discrete algebra, not a continuum GR claim, and does not itself invoke the RS forcing chain (T0–T8) or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.