e_331120
plain-language theorem explainer
Pointwise kernel check: the folded midpoint numerator at multi-index (3,3,1,1,2,0) equals eight times the explicit integer table entry. Gravity analysts cite it only as one cell of the 256-case Fin-4 grid that assembles the global m2Num = 8·explicitZ identity. Proof is a single decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,3,1,1,2,0)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(3,3,1,1,2,0)=8\,Z(3,3,1,1,2,0)$.
background
This module sits in the 4D Regge exact-midpoint analysis for the M2 TT identity. The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add each contribution $\mathrm{contrib},t,a,b,c,d,i,j$. The comparison target $Z=\mathrm{explicitZ}$ is a sparse integer table on $(\mathbb{F}_4)^6$ (typical nonzero values $\pm 2,,4$).
The local setting is chunk 15 of a 256-way kernel partition: every sextuple of Fin-4 indices is discharged by a separate decide lemma so the assembler can recombine them without a monolithic proof term. Upstream, only the two defs $N$ and $Z$ are required; no analytic lemma is invoked at this cell.
proof idea
One-line computational discharge: by decide. Both sides reduce to concrete Int values once the six Fin-4 arguments are substituted, so the kernel equality is a pure integer decision with no tactic branching or named lemmas.
why it matters
Feeds the universal assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; N=8Z$ and proves it by exhaustive fin_cases on the six indices. Each chunk lemma such as this one supplies one concrete cell so the assembler stays small and checkable.
In the broader gravity stack this identity is bookkeeping for the exact midpoint form of the 4D Regge M2 TT kernel: once $N=8Z$ holds pointwise, closed-form evaluations of the midpoint contribution become available without re-folding the coupling list. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is pure discrete kernel certification inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.