e_101331
plain-language theorem explainer
Pointwise identity: the folded Regge M2TT numerator at multi-index (1,0,1,3,3,1) equals eight times the explicit integer table at that same point. Gravity analysts cite it when assembling the full six-index kernel identity. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(1,0,1,3,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(1,0,1,3,3,1)=8\,Z(1,0,1,3,3,1)$.
background
This module is chunk 4 of a 256-way kernel split proving $N=8Z$ pointwise on $(\mathrm{Fin},4)^6$ for the exact midpoint M2TT identity in 4D Regge analysis.
The numerator $N=\mathrm{m2Num}$ is the fold of coupling contributions over a fixed list: it sums $\mathrm{contrib}$ terms at a six-index slot. The closed form $Z=\mathrm{explicitZ}$ is an explicit integer-valued table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on distinguished patterns).
The local goal is mechanical certification that the fold matches $8Z$ at every concrete multi-index, so a later assembler can reassemble the universal statement without re-deriving the algebra.
proof idea
One-line computational proof: decide. Both sides reduce at the concrete indices $(1,0,1,3,3,1)$ to closed integers (the fold evaluates; the table lookup evaluates), and the kernel checks the integer equality $N=8Z$ by decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem $\mathrm{m2Num_eq_eight_explicitZ}$, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by exhaustive $\mathrm{fin_cases}$ on all six indices. Each chunk theorem such as this one discharges one concrete branch of that case split.
In the gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge calculus: it certifies that the folded coupling numerator is exactly eight times a sparse explicit table, clearing a numerical bottleneck before continuum or continuum-limit arguments. It is infrastructure, not a forcing-chain landmark (T0–T8), but it is required scaffolding for trustworthy 4D Regge identities in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.