e_012133
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at index sextuple (0,1,2,1,3,3) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full 4D Regge midpoint M2 TT numerator identity over all Fin-4 indices. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,1,3,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,1,2,1,3,3)=8\,Z_{\mathrm{expl}}(0,1,2,1,3,3)$.
background
This module is chunk 1 of a 256-case kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times an explicit integer table. The ambient setting is discrete gravity analysis: couplings on Fin-4 index sextuples are summed, then matched to a closed form.
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 comparison target $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive case table (sample entries include $4$, $-2$, and so on for distinguished patterns).
The local claim is one concrete sextuple in that table-versus-fold comparison. Sibling declarations cover the other index patterns in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of couplingZList contributions at $(0,1,2,1,3,3)$; the right-hand side looks up explicitZ at the same sextuple and multiplies by 8. The kernel closes the integer equality with no further lemmas.
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_{\mathrm{expl}}$ by exhausting Fin-4 cases. That global identity is the certified numerator half of the Regge exact midpoint M2 TT relation in 4D discrete gravity inside the Recognition Science gravity stack.
Without the pointwise chunk facts, the assembly cannot discharge every index pattern. The module doc frames the work as "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)"; this declaration is one of those decides. It does not itself touch the forcing chain (T0–T8) or the J-cost, but it hardens the discrete-gravity side that later couples to continuum limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.