e_013102
plain-language theorem explainer
For the six-index slot (0,1,3,1,0,2) on Fin 4, the folded M2 numerator equals eight times the explicit closed-form table entry. Gravity analysts certifying the 4D Regge midpoint M2 TT identity cite this as one atomic kernel cell. The proof is a single kernel decide on concrete integers.
Claim. With indices $(a,b,c,d,i,j)=(0,1,3,1,0,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel that checks the identity $m_2^{\mathrm{num}}=8\cdot Z$ pointwise on six $\mathrm{Fin},4$ indices. The setting is the exact midpoint form of the 4D Regge M2 TT identity used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution at the six indices. The comparison target $Z$ is an explicit integer table on the same six indices (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The full quantified statement is assembled downstream by exhausting all index tuples; each chunk theorem such as this one discharges one concrete cell.
proof idea
One-line kernel proof: decide evaluates both sides as concrete Int values (the fold that defines the numerator versus eight times the matching table clause) and closes the equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states $\forall$ six indices, numerator equals eight times the table, and proves it by nested fin_cases on all six $\mathrm{Fin},4$ arguments. Each case lands on a chunk cell of this form; this declaration is the cell for $(0,1,3,1,0,2)$.
In the Recognition gravity stack, that global identity is the algebraic certificate that the midpoint M2 TT numerator matches its closed form before continuum or continuum-limit arguments. It is pure discrete bookkeeping on the Regge side, not a forcing-chain (T0–T8) step, but it is required scaffolding for the 4D gravity identities that sit above the discrete kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.