e_120032
plain-language theorem explainer
Kernel identity for one of 256 index sextuples: the folded Regge coupling numerator at (1,2,0,0,3,2) equals eight times the explicit integer table at those indices. Gravity analysts assembling the 4D midpoint M2 TT identity cite these chunks. Proof is a single computational decide on concrete Fin-4 values.
Claim. For the index sextuple $(a,b,c,d,i,j)=(1,2,0,0,3,2)$ with each index in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer table: $m_2^{\mathrm{num}}(1,2,0,0,3,2)=8\,Z^{\mathrm{expl}}(1,2,0,0,3,2)$.
background
This module is chunk 6 of a 256-way case split proving $m_2^{\mathrm{num}}=8,Z^{\mathrm{expl}}$ on all of $(\mathbb{F}_4)^6$. The setting is the exact midpoint analysis of the 4D Regge M2 TT identity in the Gravity.Analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add each contribution term at the six indices. The companion $Z^{\mathrm{expl}}$ is an explicit integer-valued table on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z^{\mathrm{expl}}(0,0,1,1,2,2)=4$ and $Z^{\mathrm{expl}}(0,0,1,2,1,2)=-2$).
Both definitions live in the KernelCert module; this chunk only evaluates them at one concrete point.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six $\mathrm{Fin},4$ arguments are fixed at $1,2,0,0,3,2$, so the kernel decision procedure discharges the equality with no lemmas or rewriting.
why it matters
Feeds the universal assembly theorem $m_2^{\mathrm{num}}=8,Z^{\mathrm{expl}}$ for all six indices, proved by exhaustive fin_cases over $(\mathbb{F}_4)^6$. That identity is the algebraic core of the Regge exact-midpoint M2 TT certification in 4D: it replaces the folded coupling sum by a closed integer table, scaled by eight.
Within Recognition gravity analysis this is pure bookkeeping infrastructure, not a forcing-chain step (T0–T8). It closes one cell of the 256-cell decide grid so the assemble theorem can quote a complete case cover rather than re-deciding every sextuple inline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.