e_030300
plain-language theorem explainer
Pointwise check that the folded coupling numerator equals eight times the explicit integer table at multi-index (0,3,0,3,0,0). Gravity analysts cite it as one cell of the 256-case kernel for the 4D Regge midpoint M2 identity. The proof is a single kernel decision on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,3,0,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,3,0,3,0,0)=8\,Z(0,3,0,3,0,0)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator $N=\mathrm{m2Num}$ is obtained by folding a fixed coupling list and summing a local contribution at each tuple. The comparison target $Z=\mathrm{explicitZ}$ is an explicit case table of small integers (entries such as $4$, $-2$, and so on).
The module is chunk 3 of a 256-cell kernel: every multi-index is checked separately so that a later assembly theorem can recombine them. The local claim is exactly the scalar identity $N=8Z$ at one fixed cell.
Upstream, both maps are defined in the kernel certificate module; this chunk only evaluates them at the concrete point $(0,3,0,3,0,0)$.
proof idea
One-line computational discharge: decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the case table for the explicit form, so the kernel closes the equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $N=8Z$ for every six-tuple in $(\mathrm{Fin},4)^6$ by exhausting indices. That global identity is the algebraic core of the Regge exact-midpoint M2/TT certificate in four dimensions: it replaces a summed coupling expression by a sparse closed table, scaled by eight.
Within Recognition gravity, such kernel identities underwrite discrete curvature bookkeeping on the eight-tick, $D=3$ side of the forcing chain. This cell is not conceptually deep on its own; its value is coverage. Missing any one of the 256 pointwise facts would leave a hole in the universal statement the assembly exports.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.