e_033320
plain-language theorem explainer
For the six-index tuple (0,3,3,3,2,0) on Fin 4, the folded Regge coupling numerator equals eight times the explicit closed-form kernel value. Gravity analysts checking the 4D midpoint M2 TT identity cite this as one certified cell of the 4^6 table. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,3,2,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator satisfies $m_2^{\mathrm{num}}(0,3,3,3,2,0)=8\,Z_{\mathrm{explicit}}(0,3,3,3,2,0)$.
background
This module is chunk 3 of a 256-cell kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times an explicit integer kernel. Indices run over $\mathrm{Fin},4$, labeling discrete edge/face slots in the midpoint stencil.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at those six indices. The comparison value $Z_{\mathrm{explicit}}$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (entries such as $4$, $-2$, and so on).
The local claim is only the single cell $(0,3,3,3,2,0)$. Sibling chunk theorems cover the rest of the table; the assemble theorem quantifies over all indices.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left by evaluating the fold of contrib over couplingZList at $(0,3,3,3,2,0)$, the right by multiplying the pattern-matched explicitZ entry by 8. The kernel checks integer equality; no lemmas are invoked.
why it matters
Feeds the universal identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and is proved by exhausting $\mathrm{Fin},4$ on each index. That assemble step is the certified algebraic core of the Regge exact-midpoint M2 TT identity in 4D gravity analysis inside the monolith.
In the broader Recognition stack this is bookkeeping infrastructure for discrete gravity identities, not a forcing-chain landmark (T5–T8, RCL, $\varphi$). It closes one cell of the numerator-versus-explicit-kernel table so the quantified midpoint identity can be cited without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.