e_233231
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at multi-index (2,3,3,2,3,1) equals eight times the explicit integer table at that same index. Gravity analysts assembling the 4D midpoint M2 TT identity cite this as one of 256 kernel cells. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,3,3,2,3,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer table entry: $N(2,3,3,2,3,1)=8\,Z(2,3,3,2,3,1)$.
background
This module is chunk 11 of a 256-cell kernel certifying that the folded numerator of the Regge midpoint M2 TT identity in 4D equals eight times a closed-form integer table. Indices run over $\mathbb{F}_4$ (four values), so there are $4^6=4096$ conceivable sextuples; the kernel is partitioned into decide-sized chunks.
The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at 0 and add a contribution term for each coupling entry. The table $Z$ is an explicit pattern-matched integer function on the same six $\mathbb{F}_4$ arguments (sample values include $4$, $-2$, and so on). The local claim is the scalar equality $N=8Z$ at one fixed sextuple.
Upstream, both $N$ and $Z$ live in the kernel certificate module; this chunk only evaluates them at $(2,3,3,2,3,1)$.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are substituted, so the kernel decision procedure discharges the equality with no manual algebra.
why it matters
Parent theorem is the assembled identity $\forall a,b,c,d,i,j,, N=8Z$, proved by exhaustive fin_cases on all six indices and dispatch to these chunk lemmas. Without the pointwise cells, the assemble step has nothing to invoke.
In the Recognition gravity stack this supports the exact midpoint form of the 4D Regge M2 TT identity used in discrete curvature bookkeeping. It is pure integer kernel work: no continuum limit, no phi-ladder mass formula, and no forcing-chain step (T0–T8) is invoked here. It closes one cell of the 256-decide partition named in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.