e_122033
plain-language theorem explainer
Finite-case certificate: at multi-index (1,2,2,0,3,3) the folded coupling numerator equals eight times the explicit integer kernel Z. Gravity analysts cite it when assembling the full 4D midpoint M2TT identity. The proof is a single kernel decide on concrete integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,3,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a case-split campaign proving $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of indices in $\mathrm{Fin},4$, the discrete index set for the 4D Regge midpoint M2TT kernel identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: sum of local contributions contrib over couplingZList. The comparison target explicitZ is a closed-form integer table on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
The local goal is mechanical: evaluate both sides at one concrete tuple and certify equality in $\mathbb{Z}$. Upstream definitions live in the kernel-cert module; downstream assembly glues every tuple into a single universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals: the fold defining the numerator runs over a fixed list, and explicitZ is a pattern-match table. Lean’s kernel decision procedure checks the resulting integer equality; no lemmas beyond the two definitions are required.
why it matters
Parent theorem m2Num_eq_eight_explicitZ asserts the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ by exhaustive fin_cases. This declaration discharges the single cell $(1,2,2,0,3,3)$ inside that grid (chunk 6 of the 256-decide campaign noted in the module doc).
In the Recognition gravity stack, the equality $m_2^{\mathrm{num}}=8Z$ is the algebraic backbone of the exact midpoint M2TT identity in 4D Regge calculus. Closing every cell removes a scaffolding gap between the folded coupling definition and the explicit kernel table used in continuum and discrete matching arguments. It does not itself invoke the forcing chain (T0–T8), but it is infrastructure those continuum limits rely on once the discrete kernel is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.