e_213310
plain-language theorem explainer
Pointwise integer identity: the folded M2 numerator at multi-index (2,1,3,3,1,0) equals eight times the explicit kernel Z at that same index. Gravity analysts cite it as one cell of the 4D Regge midpoint M2–TT kernel certification. The proof is a single `decide` on concrete Fin-4 data.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,3,3,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded M2 numerator coupling equals eight times the explicit integer kernel value: $m_2(2,1,3,3,1,0)=8\,Z(2,1,3,3,1,0)$.
background
This module is chunk 9 of a brute-force certification that the folded M2 numerator equals eight times an explicit integer kernel on every 4D multi-index. The ambient setting is the exact midpoint M2–TT identity for Regge-type gravity analysis in four dimensions.
The numerator m2Num is defined by folding a fixed coupling list: it sums contribution terms contrib t a b c d i j over that list, yielding an integer for each six-tuple in $(\mathrm{Fin},4)^6$. The comparison target explicitZ is a closed-form integer table on the same index set (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The full quantified claim is assembled downstream by exhausting all Fin-4 cases; each chunk theorem discharges one concrete cell.
proof idea
One-line computational proof: by decide. After unfolding the fold that defines the numerator and the pattern-match table for the explicit kernel at $(2,1,3,3,1,0)$, both sides reduce to concrete integers in Int, and the kernel decision procedure checks equality.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and proves it by six nested fin_cases over Fin 4. Each chunk cell such as this one is a leaf of that case tree (module doc: "m2Num = 8·explicitZ, chunk 9 (256 kernel decides)").
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint M2–TT relation in 4D, not a forcing-chain landmark (T5–T8) by itself. It closes one discrete obligation so the assembled kernel certificate can be cited without residual case holes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.