e_033200
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (0,3,3,2,0,0) equals eight times the explicit integer table. Gravity analysts cite it when assembling the full 4D m2Num = 8·explicitZ kernel. The proof is a single decide on concrete Int values.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,3,3,2,0,0)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,3,3,2,0,0)=8\,Z_{\mathrm{expl}}(0,3,3,2,0,0)$.
background
This module is chunk 3 of a 256-case kernel certification that the 4D Regge exact-midpoint numerator matches an explicit integer table, scaled by eight. The ambient setting is discrete gravity analysis on Fin 4 index sextuples.
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 indices. The comparison target $Z_{\mathrm{expl}}$ is a sparse explicit map $\mathrm{Fin},4^6\to\mathbb{Z}$ with hardcoded values such as $4$, $-2$, and $0$ on the complementary support.
Upstream, both definitions live in the KernelCert module; this chunk only evaluates one concrete sextuple from that pair of defs.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed at 0,3,3,2,0,0, so the kernel equality is discharged by Lean's decision procedure on Int arithmetic with no lemmas or case splits in this declaration.
why it matters
Feeds the assembly theorem 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 exhaustive fin_cases on all six indices. Each chunk theorem such as this one covers one residue class in that 4^6 grid (module doc: "256 kernel decides").
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge calculus kernel in 4D: once every pointwise match is certified, the closed form $Z_{\mathrm{expl}}$ can replace the folded sum in downstream curvature or mass-ladder estimates. It does not itself invoke the T0–T8 forcing chain; it is pure discrete-kernel algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.