e_110201
plain-language theorem explainer
Pointwise identity: the folded Regge numerator m2Num at multi-index (1,1,0,2,0,1) equals eight times the closed-form table explicitZ at the same index. Gravity analysts cite it as one atom of the 4^6 kernel that builds the global m2Num = 8·explicitZ theorem. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,1,0,2,0,1)$ 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 5 of a 256-way split of the 4D Regge exact-midpoint $M_2$ TT identity kernel. The claim under audit is the pointwise equality $m_2^{\mathrm{num}}=8Z$ on one fixed multi-index in $(\mathbb{F}_4)^6$.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at those six indices. The companion $Z$ is an explicit pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample clauses return $4$, $-2$, etc.). Both live in the kernel certificate module imported here.
The local setting is pure integer arithmetic on a finite discrete index set; no continuum limit or variational argument is invoked at this layer.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete Int values (the fold of m2Num at the fixed indices versus 8 times the matched clause of explicitZ), and Lean’s decision procedure discharges the equality. No lemmas are applied beyond the definitions of m2Num and explicitZ.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every such atom: it introduces six free $\mathrm{Fin},4$ variables and runs fin_cases on each, so this chunk supplies one of the $4^6$ leaves. That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certificate in 4D gravity analysis inside the monolith.
In the broader Recognition stack this sits in the gravity domain, supporting discrete curvature bookkeeping that must stay consistent with the forced $D=3$ spatial skeleton (T8) and the eight-tick octave (T7) once continuum limits are taken. It closes no open physics question by itself; it is scaffolding discharge for the exact discrete identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.