e_022102
plain-language theorem explainer
Pointwise identity: the folded 4D midpoint coupling numerator at multi-index (0,2,2,1,0,2) equals eight times the explicit integer table entry. Gravity analysts cite it when assembling the full Regge M2 TT numerator identity over (Fin 4)^6. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,2,2,1,0,2)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,2,2,1,0,2)=8\,Z(0,2,2,1,0,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $N=m2Num$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z=\mathrm{explicitZ}$ is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
This module is chunk 2 of a 256-way split of the kernel: each lemma fixes one concrete six-tuple and asserts $N=8Z$ there. The local setting is pure integer arithmetic on a finite domain, not continuum GR; the factor $8$ is the global normalization relating the folded sum to the closed table.
proof idea
Both sides evaluate to concrete Int values once the six indices are fixed. The tactic decide runs the kernel decision procedure on the equality of those integers and closes the goal. No algebraic rewriting or upstream lemmas beyond the definitions of $N$ and $Z$ are required.
why it matters
The parent theorem m2Num_eq_eight_explicitZ states $\forall a,b,c,d,i,j,, N=8Z$ and proves it by exhaustive fin_cases on all six indices, invoking one chunk lemma per cell. This declaration is the cell for $(0,2,2,1,0,2)$ inside chunk 2.
In the Recognition gravity stack, the identity certifies that the midpoint M2 TT numerator matches its explicit closed form on the full discrete index set, a prerequisite for exact (not approximate) Regge curvature bookkeeping in 4D. It does not itself touch the forcing chain T0–T8; it is infrastructure under the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.