e_032202
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (0,3,2,2,0,2) equals eight times the explicit Z-table entry there. Gravity analysts cite it when assembling the full 4D kernel identity over (Fin 4)^6. Proof is a single kernel decide on the two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,2,2,0,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling sum $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
This module is chunk 3 of a 256-way split that certifies $m_2^{\mathrm{num}}=8\cdot Z$ on every sextuple of $\mathrm{Fin},4$ indices arising in the 4D Regge midpoint TT kernel.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer weight at the six indices, and the fold starts from $0$. The comparison table $Z$ is an explicit case-split function $\mathrm{Fin},4^6\to\mathbb{Z}$ listing the closed-form values expected after that sum (e.g. $4$, $-2$, and sparse zeros elsewhere).
The local goal is purely arithmetic: evaluate both sides at one fixed multi-index and check equality in $\mathbb{Z}$. Upstream definitions supply the two sides; no continuum limit or curvature hypothesis enters this chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are substituted: the fold that defines $m_2^{\mathrm{num}}$ becomes a finite sum of known contributions, and $Z$ is a closed case table. Lean’s kernel decision procedure discharges the resulting integer equality with no lemmas beyond the two definitions.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every chunk by nested fin_cases on the six indices; this declaration is the branch for $(0,3,2,2,0,2)$. That global identity is the algebraic core of the Regge-exact midpoint $M_2$ TT kernel certificate in 4D gravity analysis inside the monolith.
In the Recognition framework the certificate supports discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain: exact integer identities at the midpoint keep the discrete Einstein–Regge sector free of hidden rational remainders before continuum matching. The chunk exists only to keep the decide obligations small and parallelizable; it does not itself state a physical law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.