e_211332
plain-language theorem explainer
For the six-index tuple (2,1,1,3,3,2) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts assembling the exact 4D Regge midpoint M2 TT identity cite this as one of the 256 kernel cases. The proof is a single `decide` on concrete integer arithmetic.
Claim. For indices $a{=}2,\,b{=}1,\,c{=}1,\,d{=}3,\,i{=}3,\,j{=}2$ in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(2,1,1,3,3,2)=8\,Z_{\mathrm{expl}}(2,1,1,3,3,2)$.
background
This module is chunk 9 of a 256-case kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: edge and hinge couplings on a 4-simplex lattice with midpoint evaluation of the second-moment (M2) TT sector.
m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an Int. explicitZ is the matching closed form, a pattern-matched function (Fin 4)^6 → Int with sparse nonzero entries (e.g. 4 on diagonal-type pairs, −2 on mixed pairs).
The local claim is one concrete six-tuple inside that table. Sibling lemmas cover the other tuples; the parent assembly theorem quantifies over all of (Fin 4)^6.
proof idea
One-line computational proof: by decide. Both sides reduce to ground Int expressions once the six Fin 4 arguments are substituted. Lean’s kernel decision procedure evaluates the fold that defines m2Num and the pattern match that defines explicitZ, then checks integer equality with the factor 8. No lemmas beyond the two definitions are invoked.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the identity for every (a,b,c,d,i,j) : Fin 4, proved by exhaustive fin_cases. Each leaf of that case split lands on a chunk lemma such as this one; without the chunk, the assembly cannot close.
In the broader Recognition gravity stack, the factor-of-eight identity certifies that the discrete M2 TT midpoint kernel matches its explicit algebraic normal form. That normal form is the computational backbone for exact Regge curvature bookkeeping in 4D (the dimension forced at T8). The chunking into 256 decides keeps each kernel check tiny and independently auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.