e_200000
plain-language theorem explainer
At multi-index (2,0,0,0,0,0) on Fin 4, the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite this as one of 256 pointwise certificates that feed the global N2 = 8Z identity. The proof is a single computational decide on concrete integers.
Claim. Let each index run in $\{0,1,2,3\}$. For the sextuple $(a,b,c,d,i,j)=(2,0,0,0,0,0)$, the coupling-fold numerator $N_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is part of the Gravity analysis stack for the exact midpoint Regge identity in 4D. The local setting is a 256-way case split: each theorem checks one Fin-4 sextuple for the numerical identity between two integer-valued kernels (module doc: m2Num = 8·explicitZ, chunk 8).
The numerator $N_2$ is defined by folding a fixed coupling list: start at 0 and accumulate a contribution at each coupling term for the six indices. The explicit kernel $Z$ is a pattern-matched integer table on $(\mathrm{Fin},4)^6$, with sample entries such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The claimed relation is the pointwise equality $N_2=8Z$. Chunk 8 covers one block of index combinations by pure kernel computation.
proof idea
One-line computational proof. The tactic decide evaluates both sides at the concrete indices $(2,0,0,0,0,0)$ and checks integer equality. No named lemmas are applied beyond unfolding the fold-numerator and the explicit $Z$ table; the kernel reduces the closed integer expression automatically.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $N_2(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ for every Fin-4 sextuple and is proved by exhaustive fin_cases on all six indices. That global identity is the certified algebraic core of the 4D Regge exact-midpoint mass-squared TT identity in this analysis stack.
In the Recognition gravity work, such kernel certificates lock discrete curvature bookkeeping before continuum or phenomenological claims. The file is framed as chunk 8 of 256 kernel decides. This point is closed by computation; no scaffolding remains on the equality itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.