e_301321
plain-language theorem explainer
For the six-index tuple (3,0,1,3,2,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel at those indices. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one certified kernel cell. The proof is a single computational decide on concrete integers.
Claim. For indices $a=3$, $b=0$, $c=1$, $d=3$, $i=2$, $j=1$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2 TT identity certification: the claim that the folded numerator equals eight times an explicit integer kernel on every six-tuple of Fin-4 indices (module slogan: m2Num = 8·explicitZ, chunk 12, 256 kernel decides).
The numerator is defined by folding a fixed coupling list: start at 0 and add a local contribution at each coupling term for the six indices. The explicit kernel is a total function Fin 4^6 → ℤ given by a finite pattern match (sample clauses include (0,0,1,1,2,2) ↦ 4 and (0,0,1,2,1,2) ↦ −2). Both live in the KernelCert import.
The local job is purely arithmetic: evaluate both sides at one fixed multi-index and record equality.
proof idea
One-line computational proof: decide. Both sides are closed integer terms once the six Fin-4 arguments are literals, so the kernel match and the fold over the coupling list reduce to concrete ℤ values; decide discharges the resulting numeral equality. No lemmas beyond the two definitions are invoked.
why it matters
Parent consumer is m2Num_eq_eight_explicitZ in the Assemble module, which states the identity for all six Fin-4 indices and proves it by exhaustive fin_cases on each coordinate. Each chunk theorem such as this one supplies a certified cell so the case split closes without sorry.
In the gravity stack this identity is bookkeeping for the exact midpoint M2 TT kernel in 4D Regge calculus: the factor of eight relates the folded coupling numerator to a sparse explicit table. It does not itself invoke the RS forcing chain (T5–T8), phi, or the eight-tick octave; it is infrastructure under the discrete gravity side of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.