e_222002
plain-language theorem explainer
For the discrete multi-index (2,2,2,0,0,2), the Regge midpoint numerator equals eight times the explicit integer kernel entry. Gravity analysts cite these single-cell identities when assembling the full 4D m2Num = 8·Z table. The proof is a pure kernel decision on closed integer arithmetic.
Claim. For indices $a=b=c=2$, $d=0$, $i=0$, $j=2$ ranging in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit kernel value: $N(2,2,2,0,0,2)=8\,Z(2,2,2,0,0,2)$.
background
This module is one chunk of the 4D Regge exact-midpoint identity campaign: prove cellwise that the folded coupling numerator equals eight times a closed-form integer kernel. The ambient setting is discrete gravity on a 4-index lattice (each index in Fin 4).
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing local contributions at those six indices. The explicit kernel $Z$ is a piecewise integer table on the same six Fin-4 arguments (typical nonzero entries are $\pm 2,\pm 4$). The module goal is the scalar identity $N=8Z$ on every cell; this file handles chunk 10 of the 256 kernel decides.
Upstream, both $N$ and $Z$ are pure definitions in the kernel-cert module; no analytic hypotheses are carried.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold that defines the numerator, and the matching clause or default of the explicit kernel) and checks equality in Int. No lemmas are invoked beyond the decidable equality instance on integers.
why it matters
Parent consumer is the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six Fin-4 arguments. Each chunk theorem such as this one supplies one concrete cell so the case split closes without sorry.
In the broader Recognition gravity stack, the midpoint Regge identity is bookkeeping for the discrete curvature/action side that must match continuum limits used downstream. It does not itself invoke the forcing chain (T5–T8), $\phi$-ladder masses, or the RCL; it is pure finite combinatorial certification inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.