e_020121
plain-language theorem explainer
For the single multi-index (0,2,0,1,2,1), the folded numerator m2Num equals eight times the tabulated explicitZ kernel entry. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel cells. The proof is a pure kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,1,2,1)$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,2,0,1,2,1)=8\,Z_{\mathrm{explicit}}(0,2,0,1,2,1)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the folded numerator m2Num equals eight times a sparse explicit integer kernel explicitZ on every sextuple of Fin 4 indices.
m2Num a b c d i j is defined by folding contrib over couplingZList, accumulating an Int. explicitZ is the closed-form lookup table that returns the expected integer (for example 4, -2, or 0) on each multi-index; only a few patterns are nonzero.
The local setting is pure finite enumeration: 4^6 = 4096 cells are split across chunk modules so each cell can be discharged by the kernel. Chunk 2 holds a block of those decides; this declaration is the cell at (0,2,0,1,2,1).
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold that defines m2Num at the fixed indices, the right-hand side multiplies the explicitZ table entry by 8. Lean’s decision procedure checks integer equality; no lemmas or rewriting are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all Fin 4 sextuples by fin_cases on each coordinate and dispatch into these per-cell decides. That global equality is the algebraic core of the Regge exact-midpoint M2TT identity in four dimensions: it certifies that the numerator built from the coupling list matches the sparse explicit kernel used downstream in the gravity analysis.
Within Recognition Science this sits in the gravity stack (Regge calculus / discrete curvature bookkeeping), not on the T0–T8 forcing chain itself. It is scaffolding closure for a fully enumerated identity rather than a new physical law: once every chunk cell is decided, the assemble theorem has no sorry path left.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.