e_021302
plain-language theorem explainer
Pointwise identity: the folded M2 numerator coupling at index sextuple (0,2,1,3,0,2) equals eight times the explicit Z-table value there. Gravity analysts cite it when discharging one cell of the 4D Regge midpoint kernel. Proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,3,0,2)$ 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
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six indices in $\mathbb{F}_4$ are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each triple. The comparison target is an explicit pattern-matched table $Z:\mathbb{F}_4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$ on matched pairs, $-2$ on certain crossed pairs).
The module is chunk 2 of a 256-cell decide grid establishing $m_2^{\mathrm{num}}=8Z$ pointwise. Each cell fixes one concrete sextuple so the equality is a closed integer computation, not a symbolic identity over variables.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 indices $(0,2,1,3,0,2)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $Z$ and multiplies by $8$. No lemmas beyond the two kernel 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}}=8Z$ by exhaustive fin_cases on all six indices. That global identity is the certified numerator half of the Regge exact-midpoint M2/TT kernel comparison in 4D gravity analysis. Without the chunk cells, the assemble step cannot close. Landmark link is structural (discrete 4-index kernel bookkeeping), not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.