e_032010
plain-language theorem explainer
For the multi-index (0,3,2,0,1,0) on Fin 4, the folded Regge coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts cite it as one atomic case in the 4D midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. For $(a,b,c,d,i,j)=(0,3,2,0,1,0)$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six Fin-4 indices appear. The numerator $N$ is defined by folding a fixed coupling list: start at 0 and add a local contribution at each coupling term. The companion map $Z$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
The local module is chunk 3 of a 256-way case split whose sole job is to check $N=8Z$ pointwise. Upstream, $N$ and $Z$ are the certified kernel definitions imported from the KernelCert module; no analytic closed form is assumed beyond those defs.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values for the fixed indices $(0,3,2,0,1,0)$, and the kernel checks equality. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhausting Fin-4 cases. That global identity is the algebraic core of the Regge exact midpoint M2/TT relation in four dimensions. Within Recognition gravity, it is bookkeeping infrastructure for the discrete curvature side, not a forcing-chain landmark (T5–T8) by itself. It closes one cell of the 256-kernel decide grid announced in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.