e_310213
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (3,1,0,2,1,3) equals eight times the explicit integer kernel Z at those same indices. Gravity analysts cite it as one cell of the 256-case kernel table that certifies m2Num = 8·explicitZ. The proof is a pure decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,0,2,1,3)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, i.e. the four discrete directions of a 4D simplicial edge labeling.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add, for each coupling term $t$, the integer contribution of $t$ at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The local claim is only the single cell $(3,1,0,2,1,3)$; the surrounding siblings cover the other cells of the same chunk.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed, so the kernel decision procedure discharges equality with no lemmas and no case split inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices, invoking one cell theorem per case. That global identity is the algebraic backbone of the exact midpoint $m_2$ TT identity in 4D Regge analysis used on the gravity side of the Recognition stack. It does not itself touch the forcing chain (T5–T8) or the RCL; it is pure discrete-kernel bookkeeping supporting the continuum limit match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.