e_132001
plain-language theorem explainer
At multi-index (1,3,2,0,0,1) the Regge midpoint m₂ numerator equals eight times the explicit Z kernel entry. Gravity analysts cite it when stitching the full m₂Num = 8·explicitZ identity over (𝔽₄)⁶. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,3,2,0,0,1)$ in $(\mathbb{F}_4)^6$, the integer $m_2$ numerator equals $8$ times the explicit $Z$ value: $m_2(1,3,2,0,0,1)=8\,Z(1,3,2,0,0,1)$.
background
This module is chunk 7 of a 256-way case split proving $m_2\mathrm{Num}=8\cdot\mathrm{explicitZ}$ on every 6-tuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint identity for the 4D Regge $m_2$ TT kernel in the Gravity analysis layer.
Upstream, $m_2\mathrm{Num}(a,b,c,d,i,j)$ is the fold of coupling contributions over a fixed coupling list, returning an integer. $\mathrm{explicitZ}$ is the closed-form integer kernel on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on for distinguished index patterns).
The local claim is one concrete instance of that equality, chosen so a decision procedure can discharge it without symbolic algebra.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,3,2,0,0,1)$. The left side reduces the fold defining $m_2\mathrm{Num}$; the right side multiplies the looked-up $\mathrm{explicitZ}$ entry by $8$. Integer equality is then decided in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem $m_2\mathrm{Num_eq_eight_explicitZ}$ assembles every index tuple into the global identity $\forall a,b,c,d,i,j,; m_2\mathrm{Num}=8\cdot\mathrm{explicitZ}$. This chunk entry is one of the decided cells that make that universal statement hold by exhaustive case analysis on $\mathrm{Fin},4$.
In the Recognition gravity stack the identity certifies that the midpoint Regge $m_2$ numerator is exactly eight times the explicit $Z$ kernel, a bookkeeping step toward the 4D TT midpoint formula. It does not itself touch the forcing chain (T0–T8) or the RCL; it is pure discrete kernel arithmetic supporting the continuum limit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.