e_321231
plain-language theorem explainer
At Fin-4 indices (3,2,1,2,3,1), the folded M2 numerator equals eight times the explicit Z coupling entry. Gravity analysts building the 4D Regge midpoint M2-TT identity cite it as one kernel case among the chunked decides. Proof is a single decide evaluating both integer sides.
Claim. For indices $a=3$, $b=2$, $c=1$, $d=2$, $i=3$, $j=1$ in $\{0,1,2,3\}$, the M2 numerator obtained by folding coupling contributions equals $8$ times the explicit integer Z-table value at those indices: $m_2^{\mathrm{num}}(3,2,1,2,3,1)=8\,Z(3,2,1,2,3,1)$.
background
In the 4D Regge midpoint M2-TT analysis, six discrete indices run over Fin 4 (vertex/simplex labels). The M2 numerator is the integer fold of a fixed coupling-contribution list at those indices. The explicit Z map is a closed-form pattern-matched Int table packaging the same coupling data without the fold (sample entries 4, -2, ...).
This module is chunk 14 of the kernel certificates that establish the pointwise relation numerator = 8 · explicit Z. The assembly theorem then quantifies over every index sextuple by exhaustive fin_cases, discharging each concrete sextuple with one of these decides. Local setting: pure integer identities supporting exact discrete curvature bookkeeping before any continuum limit.
proof idea
One-line computational certificate: decide reduces both sides to concrete integers. The left side evaluates the fold of contrib over couplingZList at (3,2,1,2,3,1); the right side multiplies the matched explicitZ entry by 8. Equality of the two Int values is checked by the kernel. No intermediate lemmas beyond the two definitions.
why it matters
Direct input to the universal statement that the M2 numerator equals eight times explicit Z for every Fin-4 sextuple. That parent theorem is proved by nested fin_cases, each leaf a chunk decide such as this one, and is the algebraic core of the Regge exact midpoint M2-TT identity certificate in 4D. In the Recognition gravity stack it locks discrete mass/coupling bookkeeping on the lattice side. It does not itself touch continuum GR, the forcing chain T0-T8, or the phi-ladder mass formula; it is infrastructure for the exact discrete identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.