e_032233
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (0,3,2,2,3,3) equals eight times the explicit integer table at those same indices. Gravity analysts cite it when assembling the full Fin-4^6 midpoint M2 numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,3,2,2,3,3)$ with each coordinate in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit closed-form integer: $N(0,3,2,2,3,3)=8\,Z(0,3,2,2,3,3)$.
background
This module is chunk 3 of a 256-case kernel certification that the midpoint M2 numerator in the 4D Regge analysis equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. ${0,1,2,3}$.
The numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list and summing a local contribution at each six-index slot. The table $Z=\mathrm{explicitZ}$ is a pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on). The local claim is the scalar equality $N=8Z$ at one concrete tuple.
Upstream, both $N$ and $Z$ live in the kernel certificate module; this chunk only evaluates them at fixed arguments.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are literals, so the kernel equality checker discharges $N(0,3,2,2,3,3)=8,Z(0,3,2,2,3,3)$ with no manual algebra.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ on $(\mathrm{Fin},4)^6$ and is proved by exhaustive fin_cases. Each chunk theorem such as this one is a named, machine-checked cell in that grid (module doc: "m2Num = 8·explicitZ, chunk 3 (256 kernel decides)").
In the gravity stack this identity is bookkeeping for the exact midpoint M2/TT analysis in 4D Regge calculus: it certifies that the folded coupling numerator matches the closed form used downstream. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete linear-algebra support inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.