e_023320
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,2,3,3,2,0) equals eight times the explicit integer table at that same point. Gravity analysts cite it as one kernel cell in the 4D midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(0,2,3,3,2,0)\in(\mathrm{Fin}\,4)^6$, the summed coupling numerator equals eight times the explicit closed-form integer: $m_2^{\mathrm{num}}(0,2,3,3,2,0)=8\,Z_{\mathrm{expl}}(0,2,3,3,2,0)$.
background
This module is chunk 2 of a 256-cell kernel certification that the 4D Regge midpoint numerator m2Num is identically eight times a sparse explicit integer table explicitZ. Both live in the KernelCert module.
m2Num a b c d i j folds couplingZList, accumulating each term's contribution contrib t a b c d i j into an Int. explicitZ is a pattern-matched table on six Fin 4 indices, returning small integers such as $4$, $-2$, and (implicitly) $0$ off the listed patterns.
The local goal is purely arithmetic: evaluate both sides at one fixed sextuple and check equality. No continuum limit or curvature hypothesis enters here; the physics content sits in the parent assembly that these cells feed.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete Int values (the fold over a finite list versus a table lookup), so the decidable equality checker discharges the goal with no lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ and proves it by exhaustive fin_cases on all six indices, routing each cell to a chunk theorem of this form.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge calculus: once the numerator matches the closed table everywhere, downstream curvature and continuum comparisons can quote a single closed form instead of a fold. It does not itself touch the forcing chain (T0–T8) or the J-cost; it is infrastructure under the discrete gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.