e_110211
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at multi-index (1,1,0,2,1,1) equals eight times the explicit Z-table value there. Gravity analysts cite it as one kernel cell in the 4D Regge midpoint M2–TT numerator certification. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,0,2,1,1)$ 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 entry $Z(a,b,c,d,i,j)$.
background
This module is chunk 5 of a 256-cell kernel that certifies, index by index, the identity $m_2^{\mathrm{num}}=8\cdot Z$ for the 4D Regge exact-midpoint M2–TT analysis.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib evaluated at the six $\mathbb{F}_4$ indices. The comparison table $Z$ is an explicit integer-valued function on $(\mathbb{F}_4)^6$, given by a finite pattern match (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both objects live in the kernel certificate module imported here; the present theorem only evaluates one concrete sextuple.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathbb{F}_4)^6$ by exhausting all indices with fin_cases. Each chunk theorem such as this one discharges one cell of that $4^6=4096$-case (here organized as 256 kernel decides) grid.
In the gravity stack this underwrites the exact midpoint M2–TT numerator identity in 4D Regge calculus, a discrete curvature/mass-squared bookkeeping step. It is pure finite arithmetic certification, not a continuum GR derivation, and sits downstream of the explicit $Z$ table and the folded coupling definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.