e_222012
plain-language theorem explainer
Pointwise check that the M2 numerator equals eight times the explicit Z-kernel at multi-index (2,2,2,0,1,2) in (Fin 4)^6. Gravity analysts cite it only as one cell of the 256-case kernel table. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=2$, $d=0$, $i=1$, $j=2$ in $\mathbb{F}_4$, the folded M2 numerator equals eight times the tabulated explicit $Z$-kernel: $m_2^{\mathrm{num}}(2,2,2,0,1,2)=8\,Z_{\mathrm{expl}}(2,2,2,0,1,2)$.
background
This module is chunk 10 of a 256-cell case split proving $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on all of $(\mathbb{F}_4)^6$. The setting is the exact midpoint identity for the 4D Regge M2/TT kernel used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer via a local contrib map, and the fold starts at 0. The comparison object $Z_{\mathrm{expl}}$ is an explicit integer table on six Fin-4 indices (sample clauses return $4$, $-2$, etc.).
The parent assembly theorem states the identity for every multi-index and discharges it by nested fin_cases, so each chunk theorem such as this one is a single concrete cell of that table.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the fixed indices $(2,2,2,0,1,2)$ to concrete integers (the fold for the numerator versus the matching clause of the explicit table, scaled by 8) and closes the equality by the kernel decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $\forall(a,b,c,d,i,j),, m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhausting Fin-4 cases. That global identity is the certified algebraic core of the 4D Regge exact-midpoint M2/TT analysis: it replaces a symbolic fold by a closed integer kernel, enabling downstream curvature and continuum-limit arguments in the gravity layer.
Within Recognition Science this is bookkeeping infrastructure for discrete gravity, not a forcing-chain landmark (T5–T8). It closes one of the 256 decide cells so the assembled equality has no sorry and no residual case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.