e_201223
plain-language theorem explainer
For the six-index tuple (2,0,1,2,2,3) on Fin 4, the folded M2 numerator equals eight times the explicit integer kernel value. Gravity analysts assembling the 4D Regge midpoint identity cite this as one of the 256 kernel decides. The proof is a single `decide` on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,2,2,3)$ with each index 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 chunk 8 of a 256-case kernel certification that the 4D Regge midpoint M2 numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. coordinate labels ${0,1,2,3}$ in a 4-simplex / 4D lattice setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (sample values include $4$, $-2$, and so on). The local claim is the pointwise identity $m_2^{\mathrm{num}}=8Z$ at one concrete multi-index.
Upstream, both $m_2^{\mathrm{num}}$ and $Z$ live in the kernel certificate module; this chunk only evaluates them at $(2,0,1,2,2,3)$.
proof idea
One-line computational proof: by decide. Lean reduces both sides at the concrete Fin-4 indices to closed integers (the fold for the numerator versus the pattern match for $Z$) and checks equality by the decision procedure. No lemmas are invoked beyond the definitions of the numerator fold and the explicit kernel table.
why it matters
Parent theorem is the assembled identity: for all six indices in Fin 4, the numerator equals eight times the explicit kernel. That assembly runs fin_cases on every coordinate and dispatches each cell to a chunk theorem of this form.
In the gravity analysis stack, the identity is the algebraic backbone of the exact midpoint M2/TT relation in 4D Regge calculus. Closing all 256 decides discharges the kernel certificate that the folded coupling matches the closed-form table, so later curvature or continuum-limit arguments can quote a single universal equality rather than a raw fold.
No open scaffold remains on this cell; it is a finished decide in the chunk partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.