e_201201
plain-language theorem explainer
For the single index sextuple (2,0,1,2,0,1) in (Fin 4)^6, the folded M2 numerator equals eight times the explicit Z-table entry. Gravity analysts cite it as one of the 256 kernel cases that assemble the global identity m2Num = 8·explicitZ. The proof is a one-line native decide on concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}1,\,d{=}2,\,i{=}0,\,j{=}1$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-case kernel certifying that the Regge midpoint M2 numerator matches an explicit integer table in 4D. Indices run over Fin 4, i.e. the discrete label set ${0,1,2,3}$ for simplex edge/vertex slots in the 4D triangulation.
m2Num a b c d i j is defined by folding couplingZList and summing the local contribution of each coupling term at those six indices. explicitZ is the closed-form integer table obtained by pattern-matching on the same six Fin 4 arguments (typical nonzero values are $\pm 2,,4$).
The local claim is the instance of $m_2^{\mathrm{num}}=8,Z$ at the concrete point $(2,0,1,2,0,1)$. Sibling theorems cover the other points in the same chunk.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are substituted into the fold definition of m2Num and the pattern table of explicitZ. Lean’s decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall(a,b,c,d,i,j:\mathrm{Fin},4),, m_2^{\mathrm{num}}=8,Z$ by exhausting all six indices with fin_cases. That global identity is the algebraic backbone of the Regge-exact midpoint M2 TT identity in 4D gravity analysis inside the Recognition Science stack.
The factor of eight is the discrete bookkeeping constant that aligns the folded coupling sum with the closed Z-table; certifying it pointwise removes a potential source of sign or multiplicity error before continuum or continuum-limit arguments. Landmark contact is indirect: the surrounding gravity analysis sits downstream of the forcing chain’s $D=3$ spatial result (T8) and the eight-tick octave (T7), which fix the discrete skeleton on which these Regge couplings live.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.