e_212213
plain-language theorem explainer
For the multi-index (2,1,2,2,1,3) with each entry in {0,1,2,3}, the folded coupling numerator equals eight times the explicit integer kernel value. Gravity analysts checking the 4D Regge midpoint M2 TT identity cite this as one cell of the 4^6 case split. The proof is a single kernel decision on the closed integer equality after both sides unfold.
Claim. At indices $a=2$, $b=1$, $c=2$, $d=2$, $i=1$, $j=3$ in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the tabulated explicit kernel integer: the left-hand side is the fold of contribution terms over the fixed coupling list; the right-hand side is the sparse case table on $(\mathrm{Fin}\,4)^6$.
background
In the 4D Regge exact-midpoint analysis two integer maps on six indices in $\mathrm{Fin},4$ are compared pointwise. The numerator side sums contribution terms by folding over a fixed coupling list. The explicit side is a sparse pattern-match table of small integers (typical nonzero entries $4$, $-2$, and similar).
The local module is chunk 9 of a 256-way kernel split whose sole job is to discharge numerator $= 8\cdot$ explicit table at concrete tuples. Upstream definitions live in the kernel-certificate module: the numerator is the fold of contributions; the explicit map is the case table on six $\mathrm{Fin},4$ arguments.
This declaration treats only the tuple $(2,1,2,2,1,3)$.
proof idea
One-line wrapper: by decide. Both sides are closed integer expressions once the numerator fold and the explicit case table are evaluated at the fixed indices; the kernel checks the resulting numeral equality. No lemmas beyond the two upstream definitions are invoked.
why it matters
The parent assembly theorem states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases on each coordinate. Chunk lemmas such as this one supply decided cells so the universal claim can be assembled without one monolithic decision. In the Recognition gravity stack this is pure algebraic certification of the discrete $M_2$ TT midpoint identity in four dimensions, a computational step toward continuum curvature weights. It does not touch the forcing chain T0-T8, the J-cost, or the phi ladder; it is kernel arithmetic under the Regge analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.