e_133301
plain-language theorem explainer
For the six-index cell (1,3,3,3,0,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Analysts proving the global 4D midpoint M2TT numerator identity cite this cell among the 256-decide chunks. The proof is a pure kernel decision on concrete integers.
Claim. Let $N$ be the folded coupling numerator and $Z$ the explicit integer kernel on $(\mathrm{Fin}\,4)^6$. Then $N(1,3,3,3,0,1)=8\,Z(1,3,3,3,0,1)$.
background
This module is one chunk of the discrete verification that the 4D Regge midpoint M2TT numerator equals eight times an explicit integer kernel on every six-tuple of indices in $\mathrm{Fin},4$. The module header states the goal directly: $m2Num=8\cdot explicitZ$, chunk 7, discharged by 256 kernel decides.
The numerator $N=m2Num$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each list entry for the six indices. The explicit kernel $Z=explicitZ$ is a total function $(\mathrm{Fin},4)^6\to\mathbb{Z}$ given by a finite pattern table (sample entries include $4$, $-2$, and further signed integers on matched index patterns).
The ambient setting is exact algebraic bookkeeping for a Regge-style midpoint identity in four dimensions, not a continuum curvature derivation. Upstream, both $N$ and $Z$ live in the kernel-certificate module imported here; downstream assembly will quantify over all index tuples.
proof idea
One-line computational proof: decide. After substituting the six concrete $\mathrm{Fin},4$ values, both sides reduce to closed integer expressions ($N$ via the fold of contributions, $Z$ via the pattern table), and the kernel checks equality to $8Z$. No lemmas are invoked beyond the decidable equality of the evaluated integers.
why it matters
The parent theorem is the assembled identity $\forall a,b,c,d,i,j,; N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$, proved by exhaustive fin_cases on each coordinate and discharge of each cell. This declaration is one concrete cell in chunk 7 of that case split.
In the Recognition gravity stack, such exact numerator identities underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain without floating-point remainder. The result does not itself invoke $J$, $\varphi$, or the RCL; it is pure integer certification feeding the Regge midpoint M2TT line. Closing all chunks removes scaffolding between the folded coupling definition and the explicit kernel table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.