e_021133
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at index sextuple (0,2,1,1,3,3) equals eight times the explicit Z-table value there. Gravity analysts cite it as one kernel cell in the 4D Regge midpoint M2–TT certification. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,1,3,3)$ with each coordinate in $\mathbb{F}_4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2 numerator equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions). The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each list contribution at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments, nonzero only on a short list of symmetry orbits (e.g. diagonal-type entries $\pm 4$, off-diagonal $\pm 2$).
The local claim is one concrete sextuple evaluation inside that kernel. Upstream, both sides are pure definitions in the KernelCert module; no analytic hypotheses are carried. Downstream assembly will quantify over all $4^6$ cells by exhaustive case split.
proof idea
One-line computational proof: decide. Lean reduces both sides at the closed indices $(0,2,1,1,3,3)$ to concrete integers (the fold of contrib over couplingZList versus $8$ times the matched explicitZ clause) and checks equality in the kernel. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, discharging each cell by a chunk identity of this form. That global equality is the algebraic core of the 4D Regge exact-midpoint M2–TT identity certification in the Gravity analysis stack: it replaces a folded coupling sum by a sparse closed-form table, enabling later exact midpoint and continuum-limit arguments. Within Recognition Science this sits in the discrete gravity / Regge sector that supports geometric forcing (spatial $D=3$ and related structure), not in the T0–T8 J-cost chain itself. No open sorry: the cell is fully decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.