e_002113
plain-language theorem explainer
For the six-index slot (0,0,2,1,1,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form explicitZ value. Gravity analysts cite it as one cell of the 256-way kernel that certifies the Regge midpoint M2 TT identity in 4D. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,0,2,1,1,3)=8\,Z_{\mathrm{explicit}}(0,0,2,1,1,3)$.
background
This module is chunk 0 of a 256-cell kernel that checks the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{explicit}}$ on all six-tuples of $\mathrm{Fin},4$. The setting is the exact midpoint analysis of the 4D Regge M2 TT identity used in the gravity stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib t a b c d i j. The comparison target $Z_{\mathrm{explicit}}$ is an explicit integer table on the same six indices (sample entries include $4$, $-2$, and so on for the listed patterns).
The present cell fixes the concrete multi-index $(0,0,2,1,1,3)$ and asks only whether the fold equals eight times the table value there.
proof idea
One-line computational proof: by decide. Lean reduces both sides to concrete integers (the fold of m2Num on the fixed indices versus $8$ times the matching explicitZ clause) and checks equality in the kernel. No lemmas beyond the two 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}}=8,Z_{\mathrm{explicit}}$ and discharges it by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each cell such as this one supplies the decided equality for one tuple, so the assembler can finish without re-deriving the arithmetic.
In the broader Recognition gravity analysis, that universal identity is the certified algebraic core of the Regge exact-midpoint M2 TT relation in 4D. It is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8), but it is required before continuum or continuum-limit gravity statements that quote the midpoint identity can be trusted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.