e_210313
plain-language theorem explainer
Pointwise check that the folded coupling numerator at multi-index (2,1,0,3,1,3) equals eight times the explicit integer table entry. Gravity analysts cite it as one of 256 kernel cells in the Regge midpoint M2 TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,1,0,3,1,3)$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals $8$ times the explicit closed-form integer at those indices.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on sextuples of $\mathrm{Fin},4$ indices are compared. The numerator is obtained by folding a fixed coupling list and summing each term's contribution at $(a,b,c,d,i,j)$. The explicit form is a sparse case table of small integers (entries such as $4$, $-2$, and so on) that is meant to be the closed form of that sum divided by eight.
This module is chunk 9 of the 256-cell kernel: each cell fixes one concrete sextuple and asserts numerator $= 8\cdot$ explicit value. The local setting is pure integer arithmetic on a finite index set, with no continuum limit or metric ansatz left open inside the chunk.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(2,1,0,3,1,3)$ and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit table.
why it matters
Feeds the assembly theorem that states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhausting indices. That global equality is the algebraic content of the Regge exact-midpoint M2 TT identity in four dimensions: the coupling fold collapses to eight times a sparse explicit integer kernel. Within Recognition gravity, such kernel identities underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain, here specialized to the 4D midpoint calculus. The chunk closes one cell of the 256-decide cover; it does not itself address continuum recovery or observational gravity fits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.