e_121102
plain-language theorem explainer
Pointwise check that the midpoint Regge numerator equals eight times the closed-form integer table at the Fin-4 sextuple (1,2,1,1,0,2). Gravity analysts cite it only as one cell of the 256-case kernel that assembles the global identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,1,1,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(1,2,1,1,0,2)=8\,Z_{\mathrm{expl}}(1,2,1,1,0,2)$.
background
This module is chunk 6 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ on every sextuple of $\mathrm{Fin},4$ indices. The setting is the exact midpoint identity for the 4D Regge $M_2$ TT block used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: each term contributes an integer weight depending on the six indices, summed from zero. The comparison table $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The global claim is assembled downstream by exhaustive fin_cases over all six indices; each chunk theorem discharges one concrete cell so the kernel stays small enough for decide.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(1,2,1,1,0,2)$. The left side reduces by unfolding the fold over couplingZList and summing the integer contributions; the right side multiplies the matched explicitZ clause by 8. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by six nested fin_cases over $\mathrm{Fin},4$, each leaf a chunk identity of this form. Without the pointwise cells, the midpoint Regge $M_2$ TT exact identity cannot be certified in 4D.
In the broader Recognition gravity stack this identity is bookkeeping infrastructure: it replaces a summed coupling expression by a closed integer table, so later curvature and continuum-limit arguments can quote a single explicit factor of 8 rather than re-folding the coupling list. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; those enter only when the certified $M_2$ block is tied back to the phi-ladder and eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.