e_330132
plain-language theorem explainer
For the concrete multi-index (3,3,0,1,3,2) in (Fin 4)^6, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two fully evaluated integers.
Claim. For $a=3$, $b=3$, $c=0$, $d=1$, $i=3$, $j=2$ as elements of $\mathrm{Fin}\,4$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding the coupling list equals $8$ times the explicit kernel integer $Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: it records that the folded numerator equals eight times an explicit integer kernel, case by case over $(\mathrm{Fin},4)^6$. The module header states the goal as "$m2Num = 8\cdot explicitZ$, chunk 15 (256 kernel decides)."
The numerator $m2Num(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating integer contributions at each multi-index. The comparison value $explicitZ$ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$). Both live in the kernel-certificate module imported here.
The ambient setting is discrete Regge-style gravity analysis in four dimensions: one checks an exact algebraic identity between a summed coupling numerator and a closed-form kernel, index by index, before assembling the universal statement.
proof idea
One-line kernel proof: decide. Both sides are closed integer terms once the six $\mathrm{Fin},4$ arguments are substituted, so the equality reduces to a decidable proposition on $\mathbb{Z}$ and is discharged by the kernel with no lemmas or rewriting.
why it matters
The parent theorem is $m2Num_eq_eight_explicitZ$ in the assemble module, which asserts
$\forall a,b,c,d,i,j:\mathrm{Fin},4,; m2Num,a,b,c,d,i,j = 8\cdot explicitZ,a,b,c,d,i,j$
and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one concrete cell of that $4^6$-fold case split (chunk 15 of the decide grid).
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge analysis: once every multi-index satisfies the factor-of-eight relation, the assembled universal equality can be cited without residual case obligations. It does not itself touch the forcing chain (T0–T8), RCL, or the $\varphi$-ladder; it is pure discrete-kernel certification downstream of those structural claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.