e_100211
plain-language theorem explainer
At multi-index (1,0,0,2,1,1) on (Fin 4)^6, the folded Regge coupling numerator equals eight times the explicit integer table. Gravity analysts cite it as one kernel point in the 4D midpoint M2 TT identity. The proof is a single native decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,0,2,1,1)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(1,0,0,2,1,1)=8\,Z_{\mathrm{expl}}(1,0,0,2,1,1)$.
background
This module is chunk 4 of a 256-point kernel certification that the 4D Regge midpoint numerator $m_2^{\mathrm{num}}$ agrees with eight times an explicit integer table $Z_{\mathrm{expl}}$. Both maps take six arguments in $\mathrm{Fin},4$ (discrete 4D index legs) and return an Int.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution contrib t a b c d i j. The companion $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six indices (sample clauses send $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is the single-point identity at $(1,0,0,2,1,1)$. Sibling theorems cover the other concrete tuples in this chunk; the assemble layer quantifies over all of $(\mathrm{Fin},4)^6$.
proof idea
One-line computational proof: decide. After the six Fin 4 arguments are substituted, both sides reduce to concrete integers (the fold for the numerator versus the table lookup, scaled by 8), and Lean’s decision procedure checks equality. No lemmas are invoked beyond the unfolding of m2Num and explicitZ.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhausting all $\mathrm{Fin},4$ cases. That global identity is the certified algebraic core of the 4D Regge exact-midpoint M2 TT analysis in the Gravity domain.
In the Recognition framework this sits inside the discrete gravity / Regge calculus layer that supports continuum limits consistent with the forced $D=3$ spatial dimensions (T8) and the eight-tick octave structure (T7). It does not itself touch the J-cost or $\varphi$-ladder mass formula; it is pure index algebra clearing a numerator identity needed before continuum or phenomenological claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.