e_312332
plain-language theorem explainer
For the single multi-index (3,1,2,3,3,2) on Fin 4, the folded numerator coupling equals eight times the explicit integer kernel entry. Gravity analysts cite it when discharging one cell of the 4D Regge midpoint M2–TT identity. The proof is a pure kernel decision: both sides evaluate to the same integer.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}2,\,d{=}3,\,i{=}3,\,j{=}2$ in $\mathrm{Fin}\,4$, the folded numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-way split that certifies, cell by cell, the algebraic identity $m_2^{\mathrm{num}}=8Z$ on all sextuples of indices in $\mathrm{Fin},4$. The setting is the exact midpoint evaluation of the 4D Regge M2–TT kernel used in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start from 0 and add each local contribution at the six indices. The comparison object $Z$ is an explicit integer-valued table on $(\mathrm{Fin},4)^6$, given by a large pattern-match (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The present declaration fixes one concrete sextuple and asserts numerical equality of the two sides at that point.
proof idea
One-line decide. Both the fold that defines the numerator and the pattern-match that defines the explicit kernel are closed integer computations on concrete Fin 4 values, so the kernel reduces each side to a numeral and checks equality.
why it matters
The parent theorem is the universal statement that $m_2^{\mathrm{num}}(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ for every sextuple in $\mathrm{Fin},4$. That assembler runs nested fin_cases on all six indices and lands each residual goal on a chunk lemma of this form.
Chunk 13 (this file) supplies one block of those residual equalities. Together the chunks close the exact midpoint M2–TT identity in 4D, a computational certificate inside the Recognition gravity analysis layer. The identity is pure discrete algebra on the Regge kernel; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it underwrites later continuum and continuum-limit arguments that do.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.