e_013232
plain-language theorem explainer
For the concrete index sextuple (0,1,3,2,3,2) in (Fin 4)^6, the folded coupling numerator m2Num equals eight times the explicit integer kernel explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 TT identity. The proof is a single kernel decide on two closed integer terms.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,3,2)$ with each coordinate in $\mathbb{F}_4$, the summed coupling numerator equals eight times the explicit integer kernel value at those indices: $N(0,1,3,2,3,2)=8\,Z(0,1,3,2,3,2)$.
background
This module is chunk 1 of a 256-cell decide grid establishing the pointwise identity between two integer-valued kernels on $(\mathrm{Fin},4)^6$ that appear in the 4D Regge exact-midpoint M2 TT analysis.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: it accumulates every contribution $\mathrm{contrib},t,a,b,c,d,i,j$ and returns an $\mathbb{Z}$ total. The comparison kernel $Z=\mathrm{explicitZ}$ is an explicit pattern-matched table $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample entries include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local claim is the single cell of $N=8Z$ at $(0,1,3,2,3,2)$. Sibling theorems cover the remaining cells of the same chunk.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers (the fold for m2Num at fixed indices, and the matching clause of explicitZ), so the equality is a closed $\mathbb{Z}$ decision problem discharged by the kernel with no lemmas or case splits in the source.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,;\mathrm{m2Num},a,b,c,d,i,j=8\cdot\mathrm{explicitZ},a,b,c,d,i,j$ and proves it by exhaustive fin_cases on all six indices. Each cell theorem such as this one is the decide obligation that those case splits ultimately hit.
In the broader gravity stack this identity certifies that the folded coupling numerator is exactly eight times the explicit midpoint kernel, a numerical step inside the 4D Regge exact-midpoint M2 TT analysis. It is pure discrete bookkeeping: no continuum limit, no physical constant identification, and no link to the T0–T8 forcing chain beyond sitting in the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.