e_013312
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at indices (0,1,3,3,1,2) equals eight times the explicit integer table at those same indices. Gravity analysts cite it as one kernel cell in the 4D Regge midpoint M2TT certification. The proof is a single `decide` on concrete integers.
Claim. For the index sextuple $(0,1,3,3,1,2)\in(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,1,3,3,1,2)=8\,Z_{\mathrm{expl}}(0,1,3,3,1,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin 4 indices are compared. The numerator m2Num is the fold of a coupling contribution list: it sums contrib t a b c d i j over every term t in couplingZList. The companion explicitZ is a closed-form lookup table on the same six indices, returning small integers such as $4$, $-2$, and so on for the nonzero patterns.
The module is chunk 1 of a 256-cell kernel certification whose sole claim is the scalar identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ at every index sextuple. Each cell is an independent concrete equality; this declaration is the cell at $(0,1,3,3,1,2)$.
proof idea
One-line computational discharge: by decide. Both sides reduce to concrete Int values (the left via the fold definition of m2Num, the right via the pattern-match table explicitZ), and the kernel decides the equality of those integers.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all $a,b,c,d,i,j:\mathrm{Fin},4$ by exhausting the six indices with fin_cases. That universal equality is the algebraic backbone of the Regge exact-midpoint M2TT identity in four dimensions: it certifies that the summed coupling numerator is exactly eight copies of the explicit kernel, with no residual defect on any cell.
Within Recognition gravity, this is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8). It closes one of the 256 decidable cells that make the midpoint identity machine-checkable end to end.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.