e_122020
plain-language theorem explainer
One of 256 kernel equalities: the midpoint Regge m₂ numerator at multi-index (1,2,2,0,2,0) equals eight times the explicit Z table entry there. Gravity analysts assembling the full 4D identity cite it as a decided cell. The proof is a single kernel decide on concrete Fin-4 indices.
Claim. For indices $(a,b,c,d,i,j)=(1,2,2,0,2,0)$ in $(\mathbb{F}_4)^6$, the integer $m_2$ numerator equals $8$ times the explicit $Z$ value at that multi-index: $m_2(1,2,2,0,2,0)=8\,Z(1,2,2,0,2,0)$.
background
In the 4D Regge midpoint analysis, the integer kernel m2Num is the fold of coupling contributions over a fixed list: it accumulates every contrib term at a six-tuple of Fin 4 indices. The companion table explicitZ is a closed-form integer lookup on the same six-tuple domain (sample cells include values such as $4$, $-2$, and so on).
The local module is chunk 6 of a 256-cell partition of that domain. The goal of the chunk family is the pointwise identity $m_2=8,Z$ on every cell, so that a later assembler can reassemble the universal statement by exhaustive fin_cases.
No continuum geometry is invoked here: both sides are pure integer functions of discrete simplex labels.
proof idea
One-line computational proof: decide evaluates both sides at the concrete indices $(1,2,2,0,2,0)$ and checks integer equality. No lemmas beyond the definitions of the numerator fold and the explicit $Z$ table are required; the kernel reduces the closed terms directly.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2(a,b,c,d,i,j)=8,Z(a,b,c,d,i,j)$ and discharges the claim by six nested fin_cases over Fin 4. Each chunk cell such as this one is a decided leaf of that case tree.
In the broader gravity stack this identity is bookkeeping for the exact midpoint $M_2$ TT kernel in 4D Regge calculus: matching the folded numerator to eight times a sparse explicit table certifies the algebraic reduction used downstream. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.