e_322020
plain-language theorem explainer
At multi-index (3,2,2,0,2,0) the Regge midpoint numerator equals eight times the explicit integer kernel value. Gravity analysts cite it as one of the 256 pointwise checks that assemble the global m2Num = 8·explicitZ identity. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(3,2,2,0,2,0)$ 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 14 of a 256-way case split certifying that the 4D Regge exact-midpoint numerator agrees with an explicit closed-form integer kernel. The ambient setting is discrete gravity analysis: six indices in $\mathbb{F}_4$ label a coupling contribution on the midpoint lattice.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each term's contribution at the six indices. The comparison object is explicitZ, a total function $\mathbb{F}_4^6\to\mathbb{Z}$ given by a finite pattern table (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$, and so on).
The local claim is the single lattice point $(3,2,2,0,2,0)$ inside that table identity.
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the concrete Fin-4 sextuple and closes the goal. No algebraic lemmas are invoked; the kernel reduces the fold that defines the numerator and the pattern match that defines the explicit table entry to bare integers, then checks equality.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhausting all $4^6$ index tuples. This declaration discharges one of those tuples (chunk 14). The factor of eight is the structural constant relating the summed coupling numerator to the closed-form kernel used downstream in the Regge midpoint $M_2$ TT identity in 4D. It is pure discrete-gravity bookkeeping inside the Recognition gravity stack, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.