e_313231
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at index tuple (3,1,3,2,3,1) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel cells in the 4D Regge midpoint M2TT numerator certification. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,1,3,2,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 13 of a 256-cell kernel certification that the 4D Regge exact-midpoint M2TT numerator equals eight times a closed-form integer table. The ambient setting is discrete gravity analysis: couplings on a 4-index simplex skeleton are summed, then matched against an explicit formula.
The numerator m2Num is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a total function Fin 4 → ⋯ → Fin 4 → ℤ given by a finite case table (e.g. (0,0,1,1,2,2) ↦ 4, off-diagonal pairs ↦ -2, and so on).
The local claim is only the single cell with indices (3,1,3,2,3,1). Sibling theorems cover the other cells in the same chunk.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of contrib over couplingZList at the fixed six indices; the right-hand side looks up explicitZ 3 1 3 2 3 1 and multiplies by 8. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every (a,b,c,d,i,j) : (Fin 4)^6 and discharges the universal claim by exhaustive fin_cases on the six indices. Each cell theorem such as this one is the concrete witness that a particular case branch holds.
In the broader Recognition gravity stack, the certified numerator identity is infrastructure for the Regge exact-midpoint M2TT analysis in 4D (spatial dimension forced at T8). It does not itself touch the J-cost, phi-ladder, or alpha band; it is pure discrete-tensor bookkeeping needed before continuum or phenomenological claims can be stated without residual arithmetic gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.