e_312010
plain-language theorem explainer
For the six-index slot (3,1,2,0,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity in 4D cite this as one of the 256 kernel cases. The proof is a single kernel decide on integer arithmetic.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}2$, $d{=}0$, $i{=}1$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $\mathrm{m2Num}(3,1,2,0,1,0)=8\cdot\mathrm{explicitZ}(3,1,2,0,1,0)$.
background
The module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification. The numerator m2Num(a,b,c,d,i,j) is the integer obtained by folding contrib over couplingZList; it aggregates discrete curvature-coupling contributions at a six-tuple of Fin 4 indices. The companion map explicitZ is a closed-form integer table on the same six-tuples (sample values include 4, -2, and further sparse entries).
The local claim is the scalar identity m2Num = 8·explicitZ on a single fixed slot. Chunk 13 holds 256 such kernel decides; together they feed a universal quantifier over all Fin 4^6 index combinations. The setting is pure integer arithmetic on a finite discrete kernel, not continuum GR.
proof idea
One-line proof by decide. Lean reduces both sides: the left-hand fold of contrib over couplingZList at (3,1,2,0,1,0), and the right-hand 8·explicitZ at the same indices, then checks integer equality in the kernel. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ states the universal identity for all Fin 4 indices and discharges it by nested fin_cases; each case lands on a chunk theorem of this form. Without the per-slot equalities, the assemble step cannot close.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2 TT kernel in 4D Regge calculus: it certifies that the folded numerator matches eight times the explicit sparse table, so later continuum or continuum-limit arguments can quote a single closed form rather than a fold. It does not itself invoke the forcing chain (T0–T8), RCL, or phi-ladder mass formulae; it is discrete kernel hygiene upstream of those physics layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.