e_313323
plain-language theorem explainer
Kernel check that the folded M2 numerator coupling at index sextuple (3,1,3,3,2,3) equals eight times the explicit Z table entry. Gravity analysts assembling the 4D Regge midpoint TT identity cite it as one of 256 pointwise certificates. The proof is a single decidability discharge on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,3,2,3)$ in $(\mathrm{Fin}\,4)^6$, 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 13 of the 256-point kernel that certifies $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint M2 TT identity in 4D Regge analysis. Indices run over $\mathrm{Fin},4$, so the full identity is a finite table of integer equalities.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold sums them from zero. The comparison target $Z$ is an explicit case-table on the same six $\mathrm{Fin},4$ arguments, returning small integers such as $4$, $-2$, and so on.
The local goal is purely algebraic bookkeeping: show the fold matches eight times the table at one concrete sextuple, so a later exhaustive fin_cases assembly can quantify over all indices.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list versus eight times the matching explicitZ clause), and Lean’s decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by nested fin_cases on all six indices and discharge of each point by a chunk certificate such as this one.
In the gravity stack this identity is infrastructure for the exact midpoint M2 TT relation in 4D Regge calculus: the factor of eight links the summed coupling numerator to the closed-form Z table used downstream. It does not itself invoke Recognition landmarks (T5–T8, RCL, $\varphi$), but it is part of the certified discrete-geometry backbone those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.