e_021201
plain-language theorem explainer
Pointwise identity: the folded Regge midpoint numerator at multi-index (0,2,1,2,0,1) equals eight times the explicit integer table at that same point. Gravity analysts cite it as one kernel cell in the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,2,1,2,0,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit closed-form integer: $N(0,2,1,2,0,1)=8\,Z(0,2,1,2,0,1)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued kernels on six Fin 4 indices are compared. The folded numerator $N=m2Num$ accumulates, by a left fold over a fixed coupling list, every local contribution at a given multi-index. The table $Z=explicitZ$ is the matching closed-form integer pattern (sparse cases such as $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
This module is chunk 2 of a 256-cell kernel certification that $N=8Z$ holds pointwise. The local setting is pure finite enumeration: no continuum limit and no floating-point arithmetic, only exact Int evaluation on the discrete index cube.
proof idea
One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,2,1,2,0,1)$ and checks integer equality. The left side runs the fold that defines $N$; the right side looks up (or defaults) the explicit table $Z$ and multiplies by 8. No lemmas beyond the two definitions are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ on $(\mathrm{Fin},4)^6$ and discharges the claim by exhausting all index cases. Each chunk cell such as this one is a named, machine-checked witness inside that exhaustion, so the global midpoint M2–TT numerator identity rests on a finite, auditable grid rather than a schematic argument.
Within Recognition gravity, the identity is bookkeeping for the discrete curvature/coupling kernel used in the Regge-midpoint sector; it does not itself invoke the forcing chain (T5–T8) or the RCL, but it stabilizes the integer arithmetic those continuum claims later quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.