e_133232
plain-language theorem explainer
For the six-index tuple (1,3,3,2,3,2) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=1,b=3,c=3,d=2,i=3,j=2$ in $\mathrm{Fin}\,4$, the summed coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 7 of a 256-way case split proving that the Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on four-dimensional index data. Indices run over $\mathrm{Fin},4$, matching a 4D simplicial (Regge) setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: it accumulates every contribution contrib t a b c d i j over couplingZList, starting from 0. The comparison target explicitZ is a pure pattern-match table $\mathrm{Fin},4^6\to\mathbb{Z}$ with sparse nonzero entries (e.g. $4$ on diagonal-like pairs, $-2$ on mixed pairs).
The local claim is one concrete six-tuple evaluation inside that table identity, not a general algebraic derivation.
proof idea
One-line kernel proof: by decide. Lean evaluates both sides as concrete Int values for the fixed arguments $(1,3,3,2,3,2)$ and checks equality by computation. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z$ by exhaustive fin_cases on all six indices. Each chunk theorem such as this one discharges one leaf of that case tree.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint $M_2$ TT kernel in 4D Regge analysis: it certifies that the folded coupling sum collapses to a sparse closed form, so later curvature or mass-ladder arguments can quote the table rather than the fold. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete kernel certification under the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.