e_201112
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at multi-index (2,0,1,1,1,2) equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ theorem. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,1,1,2)$ in $(\mathbb{F}_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
In the 4D Regge exact-midpoint analysis, two integer kernels on six $\mathbb{F}_4$ indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the given indices. The comparison table $Z$ is an explicit case-split function $\mathbb{F}_4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$, $-2$ on selected patterns).
This module is chunk 8 of the 256 kernel decides that discharge $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The local setting is pure finite enumeration: every index lives in $\mathrm{Fin},4$, so each sextuple is a closed integer computation.
proof idea
One-line proof by decide. Lean evaluates both sides as concrete Int values: the fold that defines $m_2^{\mathrm{num}}$ at $(2,0,1,1,1,2)$, and eight times the matching clause of the explicit $Z$ table. No lemmas are invoked beyond kernel reduction of the two definitions.
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$ and proves it by six nested fin_cases over $\mathbb{F}_4$. Each chunk theorem such as this one supplies one leaf of that case tree.
In the gravity stack this identity is bookkeeping for the Regge midpoint mass-squared numerator in 4D: once every cell matches, the closed-form $Z$ table may replace the fold in downstream curvature and continuum-limit arguments. It is scaffolding closure for a finite kernel, not a new physical law; landmarks such as T8 ($D=3$) sit upstream of the 4D setup rather than in this decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.