e_320220
plain-language theorem explainer
Pointwise check that the Regge midpoint numerator m2Num at multi-index (3,2,0,2,2,0) equals eight times the closed-form kernel explicitZ at the same point. Gravity analysts cite it as one of the 256 discrete kernel decides that assemble into the full m2Num = 8·explicitZ identity. The proof is a single kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,2,2,0)$ in $(\mathrm{Fin}\,4)^6$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 14 of a 256-case kernel certification that the Regge-exact midpoint $M_2$ numerator equals eight times a closed-form integer kernel on $(\mathrm{Fin},4)^6$.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a sparse case table $\mathrm{Fin},4^6\to\mathbb{Z}$ (typical nonzero values $\pm 2,4$) encoding the closed form of that sum.
The local claim is one concrete six-tuple evaluation inside that table, not the universal statement.
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality (the fold defining $m_2^{\mathrm{num}}$ at $(3,2,0,2,2,0)$ versus $8\cdot$ the matching explicitZ clause) and accepts the ground equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the quantifiers by exhaustive fin_cases on each $\mathrm{Fin},4$ coordinate. That universal identity is the certified algebraic core of the 4D Regge-exact midpoint $M_2$ TT analysis in the Gravity domain.
Within Recognition Science this is pure discrete kernel bookkeeping for the gravity side (Regge calculus midpoint identities), not a forcing-chain (T0–T8) step. It closes one of the 256 decide cells that make the assembled equality machine-checked rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.