e_313301
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (3,1,3,3,0,1) equals eight times the explicit Z-table entry there. Gravity analysts cite it when assembling the full 4⁶ kernel certificate m₂Num = 8·explicitZ. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,3,3,0,1)$ with each coordinate in $\mathbb{F}_4$, the integer $m_2$ numerator equals $8$ times the explicit $Z$ value at that multi-index: $m_2(3,1,3,3,0,1)=8\,Z(3,1,3,3,0,1)$.
background
This module is chunk 13 of a 256-case kernel certification that the midpoint Regge $m_2$ numerator coincides with eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$ (four discrete directions in the 4D simplicial setting).
The numerator $m_2(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six-index slot. The companion table $\mathrm{explicitZ}$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the diagonal and off-diagonal patterns).
The local claim is one concrete instance of the global relation $m_2=8,Z$ asserted by the assembly theorem in the sibling assemble module.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed at $(3,1,3,3,0,1)$. Lean evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then checks integer equality in the kernel. No lemmas beyond the two definitions are required.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2=8,Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each chunk theorem such as this one supplies one (or a block of) decided cells so the assemble step can close without re-evaluating the whole fold.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $m_2$ tensor in 4D: it certifies that the summed coupling contributions match the closed Z-table used downstream in curvature and continuum-limit arguments. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure discrete-tensor algebra supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.