e_301201
plain-language theorem explainer
For the single multi-index (3,0,1,2,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 4^6 atomic cases that assemble into the global m2Num = 8·explicitZ identity. The proof is a pure kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,1,2,0,1)$ with each coordinate in $\{0,1,2,3\}$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ obtained by folding the coupling list equals $8$ times the explicit kernel value $Z^{\mathrm{expl}}(a,b,c,d,i,j)$.
background
This module sits inside the 4D Regge midpoint analysis for the M2TT identity. The numerator m2Num is defined by folding a fixed coupling list: starting from 0, each term contributes an integer contrib at the six Fin-4 indices. The comparison target explicitZ is a pattern-matched closed form on the same six indices (sample clauses return 4, -2, and so on).
The local setting is chunked verification that m2Num = 8 · explicitZ holds pointwise. With six coordinates in Fin 4 there are 4096 cases; this file is chunk 12 of the decide-driven kernel certificates. Upstream, only the two definitions are needed: the fold that builds the numerator and the explicit table that supplies the right-hand side.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted into the fold definition of the numerator and the pattern match of the explicit kernel, so the equality is a decidable statement on Int and is discharged by the kernel with no further lemmas.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which asserts the identity for every six-tuple in Fin 4 by exhaustive fin_cases. Each atomic certificate such as this one supplies a single cell of that case split, so the global algebraic identity between the folded Regge numerator and eight times the explicit kernel rests on the chunked decide family.
In the broader gravity stack this identity is bookkeeping for the exact midpoint M2TT relation in 4D Regge calculus: once numerator and explicit kernel agree up to the universal factor 8, downstream curvature and mass-window arguments can quote a closed form instead of a fold. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete tensor arithmetic supporting the gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.