e_311111
plain-language theorem explainer
For the single multi-index (3,1,1,1,1,1) in (Fin 4)^6, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 pointwise decides that assemble the global m2Num = 8·explicitZ identity. The proof is a one-shot kernel decision on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(3,1,1,1,1,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(3,1,1,1,1,1)=8\,Z_{\mathrm{explicit}}(3,1,1,1,1,1)$.
background
This module is chunk 13 of a 256-case kernel certification that the 4D Regge midpoint $M_2$ numerator agrees with an explicit closed form. The ambient setting is the exact midpoint identity for the discrete TT sector in four dimensions.
The numerator m2Num is defined by folding a fixed coupling list: it sums contrib t a b c d i j over every term t in couplingZList, yielding an integer for each six-tuple of Fin 4 indices. The comparison target explicitZ is a pattern-matched integer table on the same six indices (sample clauses include values such as $4$, $-2$, and so on).
The local claim is only the single evaluation at $(3,1,1,1,1,1)$. Sibling theorems cover the other index tuples in the same chunk.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are fixed, so the decidable equality procedure discharges $m_2^{\mathrm{num}}(3,1,1,1,1,1)=8,Z_{\mathrm{explicit}}(3,1,1,1,1,1)$ with no further lemmas.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$. Its proof runs nested fin_cases over all six indices and invokes the pointwise decides; this declaration is the case for $(3,1,1,1,1,1)$.
In the gravity analysis stack, that assembled identity certifies that the discrete Regge midpoint numerator in the 4D TT sector matches the explicit kernel used downstream. It is pure integer bookkeeping inside the discrete gravity layer, not a continuum GR statement, and does not itself touch the T0–T8 forcing chain or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.