e_121122
plain-language theorem explainer
Pointwise identity: the midpoint numerator at multi-index (1,2,1,1,2,2) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full Fin-4 kernel equality m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,1,1,2,2)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer at that multi-index: $N(1,2,1,1,2,2)=8\,Z(1,2,1,1,2,2)$.
background
In the 4D Regge exact-midpoint analysis, the numerator $N=\mathrm{m2Num}$ is the fold of a fixed coupling list: each term contributes an integer depending on six $\mathbb{F}_4$ indices. The companion table $Z=\mathrm{explicitZ}$ is a sparse explicit map $\mathbb{F}_4^6\to\mathbb{Z}$ (nonzero only on a short list of patterns such as $(0,0,1,1,2,2)\mapsto 4$).
The module is chunk 6 of a 256-way kernel split: every concrete six-tuple is discharged by decide, then reassembled. Local claim status is the single equality $N=8Z$ at $(1,2,1,1,2,2)$.
Upstream, $N$ is defined by folding couplingZList with contrib; $Z$ is the pattern-matching closed form used as the target of the identity.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the kernel equality checker closes the goal with no lemmas beyond the definitions of the numerator fold and the explicit table.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,, N=8Z$ by exhaustive fin_cases and invokes each chunk identity (including this one) on the matching branch. That global identity is the algebraic backbone of the Regge exact-midpoint $M_2$ TT kernel certification in the gravity analysis stack. It does not itself touch the RS forcing chain (T5–T8) or the J-cost; it is pure discrete tensor arithmetic supporting the continuum limit bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.