e_323200
plain-language theorem explainer
For the six-index tuple (3,2,3,2,0,0) on Fin 4, the folded midpoint numerator equals eight times the explicit kernel table entry. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of 256 kernel cases. The proof is a single kernel decide after unfolding the fold and the case table.
Claim. For indices $a=3$, $b=2$, $c=3$, $d=2$, $i=0$, $j=0$ in $\{0,1,2,3\}$, the midpoint 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 14 of a 256-case kernel certification that the folded midpoint numerator equals eight times an explicit integer table on all six Fin-4 indices. The setting is 4D Regge calculus at the exact midpoint: one needs a closed algebraic identity for the M2TT block before continuum or continuum-limit claims.
The numerator m2Num is the fold of 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^6 → ℤ given by a finite case table (e.g. (0,0,1,1,2,2) ↦ 4, several off-diagonal pairs ↦ −2, and so on). Both live in the KernelCert module imported here.
Chunk theorems such as this one pin one concrete six-tuple so the assembler can discharge the universal statement by exhaustive fin_cases without re-running the fold at the top level.
proof idea
One-line proof: by decide. Lean unfolds m2Num on the concrete indices (3,2,3,2,0,0), evaluates the fold over couplingZList, looks up explicitZ 3 2 3 2 0 0 in the case table, and checks the integer equality … = 8 * … by the kernel decision procedure. No lemmas are invoked beyond definitional reduction.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states ∀ (a b c d i j : Fin 4), m2Num a b c d i j = 8 * explicitZ a b c d i j and proves it by six nested fin_cases, each leaf a chunk decide such as this one. That universal identity is the algebraic core of the 4D Regge exact-midpoint M2TT certification in the Gravity analysis stack. Without the 256 leaf equalities, the fold-versus-table comparison stays computational rather than a closed theorem. In the broader Recognition gravity program this is scaffolding for discrete curvature identities, not a forcing-chain (T0–T8) step; it sits downstream of the geometric setup and upstream of continuum matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.