e_013210
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index tuple (0,1,3,2,1,0) equals eight times the explicit integer table at those indices. Gravity analysts cite it as one of 256 kernel cells in the 4D midpoint M2TT certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,2,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module sits in the 4D Regge exact-midpoint analysis. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six Fin 4 indices, and the fold starts from zero. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (sample clauses give values such as $4$ or $-2$ on diagonal and off-diagonal patterns).
The local goal of the chunk is the pointwise relation $m_2^{\mathrm{num}}=8Z$ on a block of the $4^6=4096$ index space, discharged by kernel decides (module doc: "m2Num = 8·explicitZ, chunk 1 (256 kernel decides)"). Upstream, only the two definitions are needed: the fold and the closed table.
proof idea
One-line computational proof: decide evaluates both sides at the concrete six-tuple $(0,1,3,2,1,0)$. The left side reduces by unfolding the fold over couplingZList; the right side multiplies the matched table entry by eight. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhausting indices. That universal equality is the algebraic core of the 4D Regge midpoint M2TT certificate in the Gravity analysis stack: it replaces a folded coupling sum by a sparse explicit integer table, scaled by eight.
Within Recognition Science this is infrastructure for discrete gravity identities on the eight-tick / $D=3$ side of the forcing chain, not a mass or $\alpha$ claim. It closes one cell of the kernel grid so the assemble step can quote a complete pointwise match rather than a partial fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.