e_000331
plain-language theorem explainer
For the single multi-index (0,0,0,3,3,1) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one of the 256 kernel cells. The proof is a pure kernel decision: Lean closes the equality by computation.
Claim. For $a=b=c=0$, $d=3$, $i=3$, $j=1$ in $\mathrm{Fin}\,4$, the summed coupling numerator at those indices equals $8$ times the explicit integer kernel entry at the same indices.
background
The module sits in the 4D Regge-calculus analysis of the midpoint M2–TT identity. The local goal, stated in the module doc, is to certify cellwise that the folded numerator equals eight times an explicit kernel table (chunk 0 of 256 decides).
The numerator is defined by folding a fixed coupling list: start at 0 and add each contribution evaluated at the six Fin-4 indices. The explicit kernel is a pattern-matched integer table on the same six indices (sample clauses return 4, −2, and so on).
Upstream, those two definitions are the only dependencies. Downstream assembly will quantify over all sextuples; this declaration discharges one concrete cell.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six concrete Fin-4 values are substituted into the fold definition and the pattern table, so the kernel evaluates the equality and closes the goal with no lemmas or rewriting.
why it matters
Parent theorem is the universal identity: for every $a,b,c,d,i,j$ in Fin 4, the folded numerator equals eight times the explicit kernel. That parent is proved by exhaustive fin_cases on all six indices; each leaf is one of these chunk decides. The present cell is the leaf for (0,0,0,3,3,1).
In the broader gravity stack this cellwise certification is bookkeeping for the exact midpoint M2–TT identity in 4D Regge analysis. It does not itself invoke the Recognition forcing chain (T5–T8) or the mass ladder; it is pure discrete-kernel algebra supporting the continuum limit arguments that sit above it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.