e_102012
plain-language theorem explainer
For the concrete index sextuple (1,0,2,0,1,2) on Fin 4, the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one cell of the 256-case kernel that certifies the 4D midpoint identity. The proof is a single native decide on fully evaluated integers.
Claim. For indices $a{=}1,b{=}0,c{=}2,d{=}0,i{=}1,j{=}2$ in $\mathbb{F}_4$, the coupling-fold numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer lookup table on six $\mathbb{F}_4$ arguments.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling triple. The comparison target is an explicit piecewise table $Z:\mathbb{F}_4^6\to\mathbb{Z}$ that returns small constants (e.g. $4$, $-2$) on named patterns and is used as the closed form.
The local module is chunk 4 of a 256-way case split: each theorem pins one concrete sextuple so that a later assembler can recombine them by exhaustive fin_cases. The identity being certified is $m_2^{\mathrm{num}}=8Z$ pointwise, a numerical bridge inside the exact midpoint mass-squared / TT analysis for discrete gravity.
proof idea
Both sides are closed integer expressions once the six Fin-4 literals are substituted: the left side reduces by folding the coupling list with the contribution rule; the right side is eight times a single table lookup. Lean’s decide tactic evaluates the equality in the integer decision procedure and closes the goal. No lemmas beyond the two kernel definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal claim $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and discharges it by six nested fin_cases over Fin 4, each leaf a chunk theorem of this form. Without the (1,0,2,0,1,2) cell, the assembler cannot finish. In the broader Recognition gravity stack this kernel equality is bookkeeping for the exact 4D midpoint Regge identity, not a forcing-chain (T0–T8) step; it keeps the discrete curvature/mass-squared algebra machine-checked so later continuum or phenomenological claims rest on a fully expanded integer table rather than an opaque fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.