e_220331
plain-language theorem explainer
Pointwise kernel identity: the folded coupling numerator at multi-index (2,2,0,3,3,1) equals eight times the explicit integer table at those same indices. Gravity analysts cite it as one of 256 concrete Fin-4 checks that assemble into the global m2Num = 8·explicitZ statement. The proof is a single decide on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(2,2,0,3,3,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit integer value: $m_2^{\mathrm{num}}(2,2,0,3,3,1)=8\,Z_{\mathrm{expl}}(2,2,0,3,3,1)$.
background
This module is chunk 10 of a 256-way split of the 4D Regge exact-midpoint M2TT numerator identity. The ambient claim is that a folded sum over a fixed coupling list equals eight times a closed integer table, pointwise on all sextuples of indices in $\mathbb{F}_4$.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and accumulating the local contribution of each term at the six indices. The comparison table $Z_{\mathrm{expl}}$ is an explicit pattern-matched function $\mathbb{F}_4^6\to\mathbb{Z}$ with a finite list of nonzero cases (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$) and zero elsewhere.
Both definitions live in the kernel-certificate module imported here. The present declaration fixes one concrete sextuple and asserts the scalar equality at that point.
proof idea
One-line computational proof: by decide. After substituting the six concrete Fin 4 indices, both sides reduce to closed integers (the fold over the finite coupling list on the left, the pattern match on the right), and Lean’s decision procedure checks equality in Int.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}4,; m_2^{\mathrm{num}}=8,Z{\mathrm{expl}}$ by exhausting all six indices with fin_cases. Each chunk such as this one discharges one residual goal in that case split (module doc: “256 kernel decides”).
In the gravity stack this identity is a numerator certificate for the exact-midpoint M2TT comparison in 4D Regge calculus. It is pure integer bookkeeping: no continuum limit, no variational argument, and no appeal to the Recognition forcing chain (T5–T8) or the RCL. Its role is to make the global eight-fold relation machine-checked rather than hand-tabulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.