e_132303
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2-numerator at multi-index (1,3,2,3,0,3) equals eight times the explicit Z-kernel integer there. Gravity analysts cite it as one cell of the 256-fold kernel table that builds the global m2Num = 8·explicitZ statement. Proof is a single decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,3,2,3,0,3)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit integer kernel value: $m_2^{\mathrm{num}}(1,3,2,3,0,3)=8\,Z(1,3,2,3,0,3)$.
background
In the 4D Regge midpoint analysis the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contribution of each coupling term at a six-index slot $(a,b,c,d,i,j)\in(\mathrm{Fin},4)^6$. The comparison object is the explicit integer kernel $Z$, a total function on the same six indices that returns a sparse pattern of small integers (typically $\pm 4,\pm 2$, or $0$).
The module is chunk 7 of a 256-way partition of that kernel. Each chunk theorem asserts the scalar identity $m_2^{\mathrm{num}}=8,Z$ at one concrete multi-index; together they underwrite the exact midpoint M2–TT identity in four dimensions.
Upstream, $Z$ and $m_2^{\mathrm{num}}$ are pure definitions in the kernel certificate module; no analytic hypothesis is required beyond the finite enumeration.
proof idea
One-line computational discharge: both sides evaluate to concrete integers once the six Fin-4 arguments are fixed, so decide closes the equality by kernel reduction and integer arithmetic. No lemmas beyond the definitions of the numerator fold and the explicit Z table are invoked.
why it matters
Feeds the assembler theorem $m_2^{\mathrm{num}}=8,Z$ for all six indices, which runs fin_cases over $(\mathrm{Fin},4)^6$ and lands on these pointwise facts. That global identity is the algebraic core of the exact midpoint Regge M2–TT certificate in 4D gravity analysis inside the monolith.
Within Recognition Science this sits in the gravity sector that checks discrete curvature bookkeeping against the forced $D=3$ spatial skeleton (forcing step T8) and the eight-tick causal octave (T7). It does not itself derive constants or the J-cost; it only certifies one numerator cell used by the continuum-limit matching arguments downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.