e_010132
plain-language theorem explainer
At multi-index (0,1,0,1,3,2), the folded numerator coupling equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of 256 kernel point checks that assemble into the global identity m2Num = 8·explicitZ on (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,1,3,2)\in(\mathrm{Fin}\,4)^6$, the folded numerator coupling $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
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices appear. The numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The companion map $Z$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that fold, up to a universal factor of eight.
This module is chunk 1 of the 256-point kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. Each sibling theorem pins one concrete multi-index; the present one treats $(0,1,0,1,3,2)$. The local setting is pure finite enumeration: no continuum limit and no floating-point arithmetic.
proof idea
One-line computational proof: decide evaluates both sides at the fixed Fin-4 sextuple and checks integer equality. The left side reduces by unfolding the fold over the coupling list; the right side reduces by the matching clause of the explicit $Z$ table (or the default zero if unmatched). No lemmas beyond kernel reduction are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the claim by nested fin_cases over all six indices, routing each leaf to a chunk theorem of this form. That global identity is the algebraic backbone of the Regge exact-midpoint $M_2$ TT certificate in 4D: once the numerator matches $8Z$ everywhere, downstream gravity identities can quote the closed table instead of the fold. Within Recognition Science this sits in the gravity analysis layer that supports discrete curvature bookkeeping consistent with the forced $D=3$ spatial setting (T8) and the eight-tick discrete time structure, though this lemma itself is purely combinatorial.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.