e_110232
plain-language theorem explainer
Pointwise identity: the folded midpoint numerator at multi-index (1,1,0,2,3,2) equals eight times the explicit integer table at the same indices. Gravity analysts cite it as one cell of the 256-case kernel that certifies m2Num = 8·explicitZ on (Fin 4)^6. Proof is a single decide on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(1,1,0,2,3,2)\in(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(1,1,0,2,3,2)=8\,Z(1,1,0,2,3,2)$.
background
This module is chunk 5 of a 256-way case split that certifies the algebraic identity between two integer-valued kernels on six Fin-4 indices in the 4D Regge midpoint analysis.
The folded numerator $N=\mathrm{m2Num}$ is defined by folding a fixed coupling list: it sums the local contribution of each coupling term at the six indices. The comparison object $Z=\mathrm{explicitZ}$ is an explicit piecewise integer table on $(\mathrm{Fin},4)^6$ (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The global claim is $N=8Z$ at every multi-index. Each chunk theorem fixes one concrete six-tuple and discharges that cell by computation.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel decision procedure checks integer equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ and proves it by exhaustive fin_cases on the six indices. That global identity is the certified bridge between the folded coupling definition and the closed-form table used downstream in the Regge midpoint $M_2$ TT analysis.
In the Recognition gravity stack this is pure discrete linear algebra on the 4D simplex index set: no continuum limit, no phi-ladder mass formula, and no forcing-chain step (T0–T8) is invoked here. It closes one of the 256 kernel cells so the assembly can treat the factor-of-eight relation as proved rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.