e_110220
plain-language theorem explainer
At multi-index (1,1,0,2,2,0) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel integer. Gravity analysts checking the 4D Regge midpoint M2 TT identity cite this as one of 256 pointwise kernel checks. Equality is discharged by a single decide on the two concrete integers.
Claim. For indices $a=1$, $b=1$, $c=0$, $d=2$, $i=2$, $j=0$ in $\{0,1,2,3\}$, the coupling-fold numerator equals eight times the explicit integer kernel: $m_2^{\mathrm{num}}(1,1,0,2,2,0)=8\,Z_{\mathrm{expl}}(1,1,0,2,2,0)$.
background
In the 4D Regge midpoint analysis, the M2 TT identity asserts that a discrete second-moment numerator built from coupling contributions matches a fixed multiple of an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$.
The numerator is the fold of a contribution map over a fixed coupling list, yielding an integer at each six-tuple. The comparison target is a piecewise integer function on the same arguments, with tabulated values (for example $4$ or $-2$) on distinguished index patterns.
This module is chunk 5 of the 256 kernel decides that discharge the pointwise equality numerator $= 8\cdot Z_{\mathrm{expl}}$. The parent assembly theorem then quantifies over all indices by exhaustive case splits on $\mathrm{Fin},4$.
proof idea
One-line computational proof: by decide. The decision procedure evaluates both sides at the fixed tuple $(1,1,0,2,2,0)$: the fold that defines the numerator, and the matching clause of the explicit kernel scaled by 8. Both reduce to concrete integers, and equality is confirmed. No intermediate lemmas are required beyond those two definitions.
why it matters
This is one atomic cell in the proof that the coupling-fold numerator equals eight times the explicit kernel for every six-tuple in $(\mathrm{Fin},4)^6$. The downstream assembly theorem introduces all six indices and closes the goal by nested fin_cases, so each concrete cell (including this one) is a required leaf.
Within Recognition Science gravity work, that full identity certifies discrete curvature bookkeeping in the 4D Regge midpoint M2 TT layer. It sits on the gravity-analysis side rather than on the forcing chain T0–T8, but it supports consistency of the discrete geometry that the eight-tick and $D=3$ constraints feed into.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.