e_330201
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (3,3,0,2,0,1) equals eight times the explicit integer kernel table at that same index. Gravity analysts assembling the 4D midpoint M2 TT identity cite these 256 chunk lemmas. The proof is a single kernel decide on concrete integer arithmetic.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,3,0,2,0,1)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(3,3,0,2,0,1)=8\,Z_{\mathrm{expl}}(3,3,0,2,0,1)$.
background
This module is chunk 15 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ on the full $4^6$ index cube for the Regge exact midpoint M2 TT identity in four dimensions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at those six Fin-4 indices. The companion $Z_{\mathrm{expl}}$ is an explicit integer-valued pattern match on the same six indices (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
Both objects live in the kernel certificate module; the present file only discharges one concrete coordinate of the equality.
proof idea
One-line proof by decide. After substituting the six concrete Fin-4 values, both sides reduce to closed integers (the fold of contrib versus the matching clause of explicitZ, scaled by 8), and the kernel checks the integer equality.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by nested fin_cases over all six indices, invoking one chunk lemma per cell. That global identity is the algebraic core of the Regge exact midpoint M2 TT certificate in 4D gravity analysis inside the monolith. No Recognition forcing-chain landmark (T5–T8, RCL, $\phi$) is touched directly; the result is pure discrete curvature bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.