e_002001
plain-language theorem explainer
For the six-index tuple (0,0,2,0,0,1) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite this as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. For $(a,b,c,d,i,j)=(0,0,2,0,0,1)$, the summed coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared. The numerator $N$ is obtained by folding a fixed coupling list and accumulating each term's contribution at the given multi-index. The explicit kernel $Z$ is a closed-form case table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
The local module is chunk 0 of a 256-way split of the identity $N=8Z$. Each chunk theorem pins one concrete six-tuple so the full universal statement can be assembled by exhaustive case split on Fin 4.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,0,2,0,0,1)$ and checks integer equality. No algebraic lemmas are invoked; the kernel reduces the fold that defines the numerator and the pattern match that defines the explicit kernel to concrete Int values and confirms they stand in the ratio eight.
why it matters
This cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the claim by nested fin_cases over all six indices. That universal identity is the certified algebraic core of the 4D Regge midpoint M2/TT relation in the Gravity analysis stack. It sits downstream of the kernel certificate definitions and upstream of any continuum or continuum-limit reading of the discrete curvature weights. Within Recognition Science gravity work it is bookkeeping infrastructure rather than a forcing-chain landmark (T0–T8), but without the cell-by-cell match the midpoint identity does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.