e_013000
plain-language theorem explainer
For the six-index slot (0,1,3,0,0,0) on Fin 4, the folded Regge midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts assembling the 4D midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,3,0,0,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module sits in the Gravity analysis layer that certifies an exact midpoint identity for the 4D Regge M2–TT kernel. The local goal, stated in the module header, is to prove $m_2=8\cdot Z$ cell by cell over a 256-point index grid (chunk 1).
The numerator $m_2$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target $Z$ is an explicit six-argument integer table on $\mathrm{Fin},4$, with sparse nonzero entries such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
Both definitions live in the KernelCert import. Downstream assembly will quantify over all six indices; the present declaration fixes one concrete tuple.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the concrete Fin-4 sextuple $(0,1,3,0,0,0)$ and checks integer equality. No lemmas are invoked beyond the reducible definitions of $m_2$ and $Z$.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,, m_2=8Z$ by exhaustive fin_cases on all six indices. Each cell such as this one discharges one branch of that case split.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint form of the 4D Regge kernel, not a forcing-chain landmark (T5–T8). It closes a finite certification obligation so later continuum or continuum-limit arguments can quote a fully proved discrete equality rather than a numerical check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.