e_231031
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (2,3,1,0,3,1) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full six-index m2Num = 8·explicitZ certificate. The proof is a single kernel `decide` on concrete Fin-4 integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,1,0,3,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table value: $N_2(2,3,1,0,3,1)=8\,Z(2,3,1,0,3,1)$.
background
In the 4D Regge midpoint analysis, two integer kernels are compared indexwise on $(\mathrm{Fin},4)^6$. The numerator $N_2=\mathrm{m2Num}$ is the fold of a coupling list: it sums contribution terms contrib t a b c d i j over couplingZList. The closed form $Z=\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
This module is chunk 11 of the 256-way kernel split that discharges $N_2=8Z$ by concrete evaluation. The local setting is pure integer arithmetic on finite indices; no continuum limit or curvature hypothesis is in play here.
Upstream, m2Num and explicitZ are defined in the kernel certificate module. The present lemma fixes one multi-index and asserts numerical equality after the factor of eight.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel decision procedure closes the equality with no lemmas or rewriting.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N_2(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and proves it by exhaustive fin_cases on the six indices. Each case lands on a chunk identity of this form.
In the Recognition gravity stack, the factor-of-eight match between the folded midpoint numerator and the explicit table is a certificate step toward the exact 4D Regge midpoint $M_2$ TT identity. It is bookkeeping, not a dynamical claim: it locks the discrete kernel so later continuum or continuum-limit arguments can quote a fully discharged integer identity rather than an open fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.