e_020001
plain-language theorem explainer
For the six-index slot (0,2,0,0,0,1) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one atomic case in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. With indices in $\{0,1,2,3\}$, the summed coupling numerator at $(0,2,0,0,0,1)$ equals $8$ times the explicit integer kernel entry at those same indices: $N(0,2,0,0,0,1)=8\,Z(0,2,0,0,0,1)$.
background
This module is one chunk of the exhaustive check that the 4D Regge midpoint numerator equals eight times a sparse explicit kernel. The ambient setting is discrete gravity analysis: six Fin-4 indices label a bilinear contribution built from a fixed coupling list.
The numerator $N=m2Num$ is defined by folding a contribution functional over couplingZList, starting from zero. The comparison target $Z=explicitZ$ is a pattern-matched integer table on six Fin-4 arguments (nonzero only on a short list of index patterns such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal slots).
Chunk 2 packages 256 such pointwise identities so the global assembly can discharge every index tuple by case split rather than by a single huge decide.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side evaluates the fold that defines the numerator at fixed indices $(0,2,0,0,0,1)$; the right-hand side multiplies the table lookup explicitZ 0 2 0 0 0 1 by eight. The kernel closes the equality with no lemmas beyond definitional reduction.
why it matters
Feeds the parent theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:, N(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and proves it by nested fin_cases over all six Fin-4 arguments, invoking one chunk identity per leaf.
That global identity is the algebraic backbone of the Regge-exact midpoint M2TT certificate in the gravity analysis stack: it replaces a folded coupling sum by a sparse closed form, enabling exact discrete curvature bookkeeping. Within Recognition Science this sits in the gravity domain supporting continuum limits and effective Newtonian structure, not in the T0–T8 forcing chain itself. No open scaffold remains at this leaf; it is a finished decide atom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.