e_321012
plain-language theorem explainer
For the single index sextuple (3,2,1,0,1,2) in (Fin 4)^6, the folded coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of the 256 kernel cells that assemble the global m2Num = 8·explicitZ identity. The proof is a one-shot kernel decision (`decide`).
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer table, one has $N(3,2,1,0,1,2)=8\,Z(3,2,1,0,1,2)$.
background
The ambient module is a 256-cell kernel certification that the 4D Regge midpoint M2 TT numerator equals eight times an explicit integer table. Indices run over Fin 4 (the four spacetime directions).
The numerator m2Num a b c d i j is defined by folding a fixed coupling list: start at 0 and add each local contribution contrib t a b c d i j. The table explicitZ is a total function (Fin 4)^6 → ℤ with hard-coded integer values on the nonzero support (e.g. 4 on diagonal-type pairs, −2 on crossed pairs) and 0 elsewhere.
Chunk 14 is one block of those 256 concrete equalities. The local claim is only the cell with indices (3,2,1,0,1,2).
proof idea
One-line computational proof: by decide. Lean reduces both sides of the integer equality (the fold that defines the numerator, and the constant 8 times the table lookup) to concrete Int values and checks they match. No lemmas are invoked beyond the definitions of the numerator and the table.
why it matters
Parent theorem is the universal identity m2Num_eq_eight_explicitZ: for every sextuple in (Fin 4)^6, the numerator equals eight times the explicit table. That assembly exhausts indices by fin_cases and lands on cells such as this one.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2 TT kernel in 4D Regge calculus: it replaces a summed coupling expression by a sparse closed-form integer table, which is what later curvature and continuum-limit arguments consume. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder; it is pure discrete-gravity algebra inside the 4D kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.