e_011102
plain-language theorem explainer
Pointwise check that the folded M2 numerator equals eight times the explicit Z-table entry at multi-index (0,1,1,1,0,2). Gravity analysts cite it as one cell of the 256-case kernel that certifies the Regge midpoint M2 identity in 4D. The proof is a single kernel decision on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,1,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint M2 TT identity in 4D Regge analysis. Indices run over $\mathrm{Fin},4$, matching four spacetime directions.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The comparison target $Z$ is an explicit integer table on $(\mathrm{Fin},4)^6$, with sparse nonzero entries such as $4$ on paired diagonals and $-2$ on selected off-diagonal patterns.
The local goal is purely arithmetic: evaluate both sides at one fixed multi-index and confirm equality of integers.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values (the fold over the coupling list versus eight times the matching table clause of $Z$), and the kernel discharges the numeral equality with no further lemmas.
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\cdot Z$ by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each chunk theorem such as this one supplies one decided cell so the universal identity closes without sorry.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2 TT coupling in 4D Regge calculus: it guarantees the folded numerator matches the closed-form $Z$ table used downstream. It does not itself invoke the forcing chain (T0–T8), $\phi$, or the eight-tick octave; it is a pure integer certification step inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.