e_312110
plain-language theorem explainer
For the six-index slot (3,1,2,1,1,0) on Fin 4, the folded Regge midpoint numerator equals eight times the explicit integer kernel value. Gravity analysts cite it when discharging one cell of the 4D m2Num = 8·Z identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,2,1,1,0)$ with each index in $\{0,1,2,3\}$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
The ambient module certifies one chunk of the exact midpoint identity for the 4D Regge/TT numerator: every six-tuple of Fin-4 indices should satisfy $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$. The numerator is defined by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The explicit kernel is a sparse integer table on those same indices (typical nonzero entries are $\pm 2,\pm 4$).
Chunk 13 is one of the 256 decide cells that cover the finite index space. Upstream, both sides are pure Int-valued functions of six Fin 4 arguments, so each cell is a closed arithmetic claim.
proof idea
One-line computational proof: decide evaluates both the folded numerator and the explicit table entry at the concrete indices $(3,1,2,1,1,0)$ and checks integer equality in the kernel. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states the identity for every six-tuple by exhausting Fin-4 cases. That global equality is the algebraic backbone of the Regge exact-midpoint M2/TT identity in 4D gravity analysis inside the monolith. The chunk pattern keeps each kernel goal tiny and independently checkable while the assemble theorem glues them into the full pointwise statement used downstream in the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.