e_302003
plain-language theorem explainer
At multi-index (3,0,2,0,0,3) the summed Regge coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite it when discharging one kernel cell of the 4D midpoint M2–TT identity. The proof is a single kernel decision (`decide`) on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(3,0,2,0,0,3)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit closed-form integer $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathbb{F}_4$ indices are compared. The numerator $N$ is defined by folding a fixed coupling list: each term contributes an integer contrib, and $N$ is their sum. The comparison target $Z$ is an explicit pattern-matched table of small integers (entries such as $4$, $-2$, and so on) on the same index domain.
The local module is one chunk of the identity $N=8Z$. The module header states the goal as "$m2Num=8\cdot explicitZ$, chunk 12 (256 kernel decides)": the full six-index space is partitioned into decidable cells, each checked by a named equality of this form.
Upstream, $Z$ and $N$ are pure definitions in the kernel certificate module; no analytic hypotheses are attached. Downstream assembly quantifies over all six indices and reduces by exhaustive fin_cases.
proof idea
One-line computational discharge: decide. Both sides are closed integer expressions once the six Fin 4 arguments are literals, so the kernel evaluates the fold defining $N$ and the table defining $Z$, then checks $N=8Z$ by native decision. No lemmas beyond the two definitions are invoked.
why it matters
This cell is one brick in the global statement m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, N=8Z$ on $(\mathbb{F}_4)^6$. That identity is the algebraic core of the Regge exact-midpoint M2–TT certificate in four dimensions: it replaces a summed coupling expansion by an eightfold multiple of a sparse explicit table, making later curvature and deficit identities purely arithmetic.
Within Recognition gravity, such kernel equalities sit under the discrete geometric layer that feeds continuum limits and the forcing chain's $D=3$ spatial readout; they do not themselves invoke $J$, $\varphi$, or the eight-tick octave, but they clear the combinatorial obstruction those landmarks later rely on. Chunk 12 is pure scaffolding closure: each e_* removes one undecided cell from the 256-decide partition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.