e_012232
plain-language theorem explainer
Pointwise identity: the folded coupling numerator at index sextuple (0,1,2,2,3,2) equals eight times the explicit integer kernel at those indices. One of 256 kernel cells assembled into the global m2Num = 8·explicitZ theorem. Proof is a single native decide on concrete Int values.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,2,3,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel certification that the 4D Regge midpoint numerator equals eight times a closed-form integer table. The ambient setting is exact midpoint identities for the discrete TT sector in four dimensions.
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 table explicitZ is a total function on six Fin 4 indices returning a hard-coded Int (typical nonzero entries are $\pm 2,\pm 4$). Both live in the kernel-cert module imported here.
The global claim is that these two agree up to the constant factor 8 at every sextuple. That claim is proved by exhaustive fin_cases over all $4^6=4096$ index tuples, each leaf discharged by a decide lemma of this form.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers (left via the fold definition of the numerator, right via the pattern-match table for the explicit kernel), and Lean’s native decision procedure checks equality.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and is proved by nested fin_cases whose leaves are exactly these e_* decides. Without the full 256-cell (per-chunk) cover, the midpoint TT identity in 4D Regge analysis would remain an unchecked table claim rather than a machine-checked equality. Sits in the Gravity analysis layer that certifies discrete curvature/mass kernels used downstream in RS gravity numerics; not itself a T0–T8 forcing step, but infrastructure for exact discrete identities those layers rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.