e_201033
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at index sextuple (2,0,1,0,3,3) equals eight times the explicit integer kernel entry. Gravity analysts assembling the 4D Regge midpoint M2 TT identity cite it as one kernel cell. Proof is a single decide on concrete integers.
Claim. For the index sextuple $(2,0,1,0,3,3)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit integer kernel value at that sextuple.
background
This module is chunk 8 of a 256-cell kernel certification that the folded midpoint numerator equals eight times an explicit integer table, in the 4D Regge exact-midpoint M2 TT identity analysis.
The numerator m2Num is the fold of a fixed coupling list: it sums a contribution functional over that list at a sextuple of Fin 4 indices. The table explicitZ is a closed-form integer function on the same sextuples (sample values include 4, -2, and other small integers on the listed patterns).
The local claim is only the cell at $(2,0,1,0,3,3)$. Sibling theorems cover the other cells in the chunk; the assembly theorem quantifies over all sextuples.
proof idea
One-line computational proof: decide evaluates both sides as concrete Int values (the fold that defines the numerator, and the matching clause of the explicit table) and discharges the equality by kernel decision. No lemmas are invoked beyond the two defining defs.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhausting all sextuples. That global identity is the algebraic backbone of the Regge exact-midpoint M2 TT certification in four dimensions: it replaces a folded coupling sum by a sparse explicit integer kernel, enabling exact midpoint identities used downstream in the gravity analysis stack. Landmark contact is structural (discrete 4-index kernel bookkeeping for the TT sector), not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.