e_230030
plain-language theorem explainer
At the six-index (2,3,0,0,3,0) the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts certifying the 4D Regge midpoint M2–TT identity cite this as one of 256 kernel cells. The proof is a single decide on concrete integer arithmetic from the two kernel definitions.
Claim. For indices $a=2$, $b=3$, $c=0$, $d=0$, $i=3$, $j=0$ in $\{0,1,2,3\}$, 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
In the 4D Regge midpoint analysis two integer kernels on six indices in $\mathrm{Fin},4$ are compared. The numerator $m_2$ folds a fixed coupling list, summing a local contribution at each multi-index. The comparison target is an explicit integer table $Z$, defined by pattern match on the six indices (sparse nonzero patterns such as $(0,0,1,1,2,2)\mapsto 4$ and several sign-flipped off-diagonal slots).
This module is chunk 11 of a 256-case kernel certification that $m_2=8Z$ pointwise. Upstream, $m_2$ is the fold of contrib over couplingZList, and $Z$ is the tabulated pattern function. The full identity is later assembled by exhaustive case splits on all six coordinates.
proof idea
One-line computational discharge: decide evaluates both sides at the concrete tuple $(2,3,0,0,3,0)$ and checks integer equality. No intermediate lemmas are invoked; the proof only unfolds the fold-definition of the numerator and the pattern table for $Z$, then closes by decidable arithmetic on $\mathbb{Z}$.
why it matters
This cell feeds the parent theorem that asserts $\forall a,b,c,d,i,j\in\mathrm{Fin},4,; m_2=8Z$. That parent is the certified algebraic core of the 4D Regge exact-midpoint M2–TT identity in the gravity analysis stack. Downstream assembly runs fin_cases on every index and discharges each residual goal by a chunk theorem of this form. The identity supplies exact discrete curvature bookkeeping for the midpoint scheme, rather than a continuum approximation. It sits inside the Gravity domain of the Recognition mirror; it does not itself touch the T0–T8 forcing chain or the RCL, but it hardens the discrete geometric layer those continuum claims eventually rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.