e_022221
plain-language theorem explainer
Pointwise identity: at index sextuple (0,2,2,2,2,1) the folded Regge midpoint numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it when assembling the full 4D kernel identity m2Num = 8·explicitZ over all Fin-4 indices. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,2,2,1)$ in $(\mathbb{F}_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 is chunk 2 of a 256-case kernel certification that the Regge exact-midpoint numerator equals eight times a sparse explicit integer table on six Fin-4 indices. The local setting is pure integer arithmetic over a fixed coupling list: no continuum limit is taken here.
The numerator m2Num is defined by folding a contribution function over couplingZList, starting from 0. The comparison target explicitZ is a pattern-matched table Fin 4^6 → ℤ with a handful of nonzero entries (e.g. 4 on diagonal-like pairs, −2 on crossed pairs) and implicit 0 elsewhere.
The identity is checked pointwise; this declaration handles one concrete sextuple in the chunk.
proof idea
One-line closed proof: by decide. Lean evaluates both sides as concrete integers (the fold of contributions versus eight times the table lookup at (0,2,2,2,2,1)) and discharges equality by kernel computation. No lemmas beyond the definitions of the numerator fold and the explicit table are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in Fin 4 by exhaustive case split. That global equality is the certified algebraic core of the 4D Regge exact-midpoint M2/TT kernel used in the gravity analysis stack.
Within Recognition Science this is bookkeeping infrastructure for discrete curvature/coupling identities on the eight-tick, D=3 lattice side of the forcing chain, not a new physical law. It closes one cell of the 256-decide grid so the assemble step can quote a complete, sorry-free pointwise match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.