e_011332
plain-language theorem explainer
For the multi-index (0,1,1,3,3,2) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=1$, $c=1$, $d=3$, $i=3$, $j=2$ in $\{0,1,2,3\}$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel entry $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint analysis: it certifies, index-by-index, that the folded numerator of the M2 tensor equals eight times a closed-form integer table. The ambient claim is the identity $m_2^{\mathrm{num}}=8,Z$ on all sextuples in $(\mathrm{Fin},4)^6$, split across 256 decide kernels.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list, accumulating each term's contribution at those six indices. The explicit kernel $Z$ is a pattern-matched integer table on the same six Fin-4 arguments (typical nonzero values $\pm 2,,4$). Both live in the kernel-certificate module imported here.
The local setting is pure finite enumeration: no continuum limit, no metric ansatz beyond the discrete index algebra of the 4D midpoint stencil.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,1,1,3,3,2)$ and checks integer equality. The left side reduces by unfolding the fold over the coupling list; the right side reduces by the pattern match on explicitZ. No lemmas beyond kernel evaluation are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhausting all Fin-4 cases. That universal identity is the algebraic core of the Regge exact-midpoint M2/TT analysis in four dimensions: it replaces a summed coupling expression by a sparse explicit table, enabling exact discrete curvature bookkeeping.
Within Recognition Gravity this is scaffolding for the discrete geometric side of the forcing chain (spatial $D=3$ plus time, eight-tick structure), not a continuum Einstein equation. It closes one of the 256 kernel cells in chunk 1 of the numerator identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.