e_010212
plain-language theorem explainer
Pointwise identity: the folded M2 numerator at multi-index (0,1,0,2,1,2) equals eight times the explicit integer kernel value at that point. Gravity analysts cite it when assembling the full 4D midpoint M2 numerator identity over (Fin 4)^6. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,2,1,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table entry: $m_2^{\mathrm{num}}(0,1,0,2,1,2)=8\,Z_{\mathrm{expl}}(0,1,0,2,1,2)$.
background
This module is one chunk of the 4D Regge midpoint M2 numerator certification: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple of Fin 4 indices (256 kernel decides in the chunk family).
Upstream, m2Num a b c d i j is defined by folding couplingZList, accumulating each term's contrib at those indices. The companion explicitZ is a closed-form integer table on the same six Fin 4 arguments (sample clauses include values such as 4 and -2 on selected diagonal and off-diagonal patterns).
The local goal is purely algebraic bookkeeping: check one concrete six-index instance of $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ so the assembly theorem can cover the full product space by cases.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed: the left-hand side evaluates the fold of contrib over couplingZList, the right-hand side looks up explicitZ and multiplies by 8. Lean’s decision procedure discharges the resulting integer equality with no further lemmas.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on the six indices. Each chunk lemma such as this one closes one residual goal in that case split (module doc: chunk 1 of the 256 kernel decides).
In the broader Gravity analysis stack this identity is infrastructure for the exact midpoint M2/TT kernel certification in 4D Regge calculus. It does not itself invoke Recognition forcing landmarks (T5–T8, RCL, phi), but it is part of the discrete-curvature bookkeeping those continuum limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.