e_200033
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,0,0,0,3,3) equals eight times the explicit integer table at that same index. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. Proof is a single decide on concrete Fin-4 integers.
Claim. For the multi-index $(2,0,0,0,3,3)\in(\mathbb{F}_4)^6$, the summed coupling numerator equals eight times the closed-form integer table: $m_2^{\mathrm{num}}(2,0,0,0,3,3)=8\,Z_{\mathrm{expl}}(2,0,0,0,3,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those indices. The companion table $Z_{\mathrm{expl}}$ is an explicit pattern-matched integer function on the same domain (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local module is chunk 8 of a 256-cell decide kernel whose sole job is to check $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at one concrete sextuple at a time. The ambient claim is the exact midpoint M2TT identity in four dimensions: after all chunks assemble, the folded numerator is identically eight times the closed form.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed at $(2,0,0,0,3,3)$, so the kernel decision procedure discharges equality with no lemmas and no case split inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}4,; m_2^{\mathrm{num}}=8,Z{\mathrm{expl}}$ and proves it by exhaustive fin_cases on the six indices. Each chunk such as this one supplies one cell of that $4^6=4096$-point (here organized as 256 kernel decides) verification grid.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge curvature kernel in 4D: it certifies that the summed coupling form collapses to a sparse explicit integer table, scaled by eight. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure discrete kernel algebra supporting the continuum gravity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.