e_010122
plain-language theorem explainer
For the six-index slot (0,1,0,1,2,2) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it when assembling the full 4D midpoint Regge M2–TT identity over all 4^6 index tuples. The proof is a single kernel decide on concrete integers.
Claim. With $a,b,c,d,i,j\in\{0,1,2,3\}$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,1,0,1,2,2)=8\,Z_{\mathrm{ex}}(0,1,0,1,2,2)$, where $Z_{\mathrm{ex}}$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over the fixed coupling list.
background
This module is one chunk of the 4D Regge midpoint M2–TT identity certification: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple in $(\mathrm{Fin},4)^6$. The module doc states the local goal as "$m2Num = 8\cdot explicitZ$, chunk 1 (256 kernel decides)."
Upstream, $m2Num(a,b,c,d,i,j)$ is defined by folding couplingZList with a contribution map contrib, starting from 0. The companion explicitZ is a pattern-matched integer table on six Fin-4 indices (sample clauses give values such as $4$, $-2$, etc.). The present theorem fixes one concrete slot in that table.
The ambient setting is discrete gravity analysis: verifying algebraic identities among Regge-style coupling numerators before they are assembled into continuum or continuum-limit statements.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete indices $(0,1,0,1,2,2)$—the fold defining $m2Num$ on the left and the pattern match for $explicitZ$ on the right—and checks integer equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,; m2Num,a,b,c,d,i,j = 8\cdot explicitZ,a,b,c,d,i,j$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one (or a block of) concrete cases inside that assembly.
In the Recognition gravity stack this is bookkeeping infrastructure for the exact midpoint M2–TT identity in 4D, not a forcing-chain landmark (T5–T8) by itself. It closes a finite kernel obligation so the assembled identity can be cited without residual sorry on this index. Open questions about continuum limits or physical mass formulae sit downstream of the assembled identity, not of this single decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.