e_032120
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (0,3,2,1,2,0) equals eight times the explicit integer table at that same point. Gravity analysts cite it as one cell of the 256-case kernel that underwrites the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,3,2,1,2,0)$ with each coordinate in $\{0,1,2,3\}$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,3,2,1,2,0)=8\,Z(0,3,2,1,2,0)$.
background
This module is chunk 3 of a 256-cell kernel certification that the folded numerator of a 4D Regge midpoint mass-squared identity equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. discrete edge/face labels in a 4-simplex combinatorics.
The numerator $N=\texttt{m2Num}$ is defined by folding a fixed coupling list: start at 0 and add a local contribution at each coupling triple for the six indices. The table $Z=\texttt{explicitZ}$ is a hand-written case map $\mathrm{Fin},4^6\to\mathbb{Z}$ (typical values $\pm 2,,4$, and zero off the listed patterns). The claim is the numerical match $N=8Z$ at one concrete six-tuple.
Upstream, both $N$ and $Z$ live in the kernel certificate module; this chunk only evaluates them at fixed arguments.
proof idea
One-line computational proof: decide. After substituting the six concrete Fin 4 literals, both sides reduce to closed integers (the fold over the coupling list on the left, the matching clause of the explicit table on the right), and the kernel checks equality. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.
why it matters
Parent theorem is the assembled global identity: for all six Fin 4 indices, the folded numerator equals eight times the explicit table. That assembly runs fin_cases on every coordinate and dispatches each cell to a chunk theorem of this form. Without the full 256-cell cover, the midpoint M2/TT identity in 4D Regge analysis lacks a certified numerator reduction.
In the Recognition gravity stack this is bookkeeping infrastructure, not a forcing-chain step (T0–T8). It closes a discrete algebraic identity needed before continuum or phenomenological claims about the Regge midpoint scheme can rest on the certified kernel. Open work sits above: using the assembled equality inside the broader TT/M2 identity, not inside this cell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.