e_022022
plain-language theorem explainer
For the multi-index (0,2,2,0,2,2), the Regge midpoint M2 numerator equals eight times the explicit kernel value Z. Gravity analysts cite it as one of the 256 finite-case certificates that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,2,0,2,2)$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(0,2,2,0,2,2)$ equals $8\,Z_{\mathrm{explicit}}(0,2,2,0,2,2)$, where $m_2^{\mathrm{num}}$ is the folded sum of coupling contributions and $Z_{\mathrm{explicit}}$ is the closed-form integer kernel.
background
This module is chunk 2 of the 256-case kernel certification that $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ on all sextuples in $(\mathrm{Fin},4)^6$. The setting is 4D Regge calculus at the exact midpoint: discrete curvature couplings are reduced to integer arithmetic so the identity can be decided rather than reasoned symbolically.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those six indices. The comparison target $Z_{\mathrm{explicit}}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (typical nonzero values $\pm 2,,4$). Both live in the kernel-cert module imported here.
Sibling lemmas $e_{020000},\ldots$ cover the other index combinations in this chunk; together they feed the exhaustive assembly.
proof idea
One-line proof by decide. Both sides evaluate to concrete integers once the six indices are fixed: the left-hand side runs the fold that defines the numerator, the right-hand side looks up (or defaults) the explicit kernel entry and multiplies by 8. Lean’s kernel checks integer equality; no lemmas or rewrites are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and discharges it by nested fin_cases over all six arguments. Each leaf is one of these chunk certificates; this declaration is the leaf for $(0,2,2,0,2,2)$.
In the Recognition gravity stack the identity is the algebraic backbone of the exact midpoint M2/TT reduction in 4D: once numerator and explicit kernel match by the factor 8, downstream curvature and continuum-limit arguments can quote a single closed form instead of a summed coupling list. It is pure finite certification, not a continuum theorem, and does not itself invoke the forcing chain (T0–T8) or the J-cost; it sits in the discrete gravity analysis layer that those continuum claims later consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.