e_322010
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (3,2,2,0,1,0) equals eight times the explicit Z-table entry. Gravity analysts cite it as one of 256 kernel cells glued by the global m₂-num assembly theorem. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,2,2,0,1,0)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer table on six $\mathbb{F}_4$ arguments.
background
This module is chunk 14 of a 256-cell kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ at every six-tuple of $\mathrm{Fin},4$ indices in the 4D midpoint Regge analysis.
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 companion table $Z$ is an explicit case-split map $\mathrm{Fin},4^6\to\mathbb{Z}$ (sample values include $4$ on diagonal pairs such as $(0,0,1,1,2,2)$ and $-2$ on mixed pairs such as $(0,0,1,2,1,2)$).
The local claim fixes one concrete cell of that six-dimensional grid, namely $(3,2,2,0,1,0)$, so both sides reduce to ordinary integers.
proof idea
One-line computational proof: decide. After substituting the six concrete Fin 4 literals, both the fold that defines the numerator and the case table for $Z$ evaluate to closed integers; Lean’s kernel decision procedure checks equality to $8$ times the table value. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the identity for every six-tuple and proves it by exhaustive fin_cases on all six indices; each leaf is one of these chunk theorems. Without the $(3,2,2,0,1,0)$ cell, the assembly cover is incomplete.
In the broader gravity stack this identity is bookkeeping for the exact midpoint $m_2$ tensor in 4D Regge calculus: the factor $8$ relates the folded coupling expansion to a sparse explicit integer kernel used downstream in curvature and continuum-limit arguments. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-tensor algebra supporting those later gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.