e_232011
plain-language theorem explainer
At multi-index (2,3,2,0,1,1) the Regge midpoint numerator m2Num equals eight times the closed-form kernel explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the full 4D identity. The proof is a single native decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,3,2,0,1,1)$ with each entry in $\mathbb{F}_4$, the integer numerator $m_2^{\mathrm{num}}(2,3,2,0,1,1)$ equals $8\,Z(2,3,2,0,1,1)$, where $Z$ is the explicit closed-form kernel on $(\mathbb{F}_4)^6$.
background
This module is chunk 11 of a 256-case kernel certification for the 4D Regge exact-midpoint $M_2$ TT identity. The ambient setting is discrete gravity on a 4-simplex skeleton: one must match a folded coupling numerator against a sparse closed form.
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 $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on $(\mathbb{F}_4)^6$ (examples: $Z(0,0,1,1,2,2)=4$, $Z(0,0,1,2,1,2)=-2$).
The local claim is the single-point equality at indices $(2,3,2,0,1,1)$. Sibling chunks cover the other $\mathbb{F}_4$ tuples.
proof idea
One-line computational proof: by decide. Both sides are closed integer terms once the six Fin 4 arguments are concrete literals, so Lean’s decision procedure evaluates the fold that defines $m_2^{\mathrm{num}}$ and the pattern match that defines $\mathrm{explicitZ}$, then checks equality to $8\cdot Z$. No lemmas are invoked beyond the two definitions.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by exhaustive fin_cases. That global identity is the algebraic core of the Regge exact-midpoint $M_2$ TT certificate in 4D.
In the Recognition gravity stack this closes a discrete curvature bookkeeping step: the folded coupling numerator is forced to the sparse kernel, so later continuum or continuum-limit arguments can quote a single closed form rather than a sum. It is pure integer algebra on the 4D index set; it does not itself invoke the T0–T8 forcing chain, but it sits inside the gravity analysis that those foundations underwrite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.