e_002121
plain-language theorem explainer
Pointwise identity: the folded Regge numerator m2Num at multi-index (0,0,2,1,2,1) equals eight times the explicit kernel table explicitZ at the same indices. Gravity analysts cite it when assembling the full Fin-4^6 identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,2,1,2,1)$ in $(\mathrm{Fin}\,4)^6$, the integer numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel value $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint 4D analysis, the numerator m2Num is the integer obtained by folding a fixed coupling list: each term contributes via a local contrib at six Fin 4 indices, and the fold starts from 0. The companion table explicitZ is a closed-form integer kernel on the same six indices (sample values include 4, -2, and other small integers on the listed patterns).
This module is chunk 0 of the 256-point kernel: one concrete equality m2Num = 8 · explicitZ per multi-index, discharged by decide. The local setting is purely combinatorial bookkeeping of that numerator against the explicit table, not a continuum GR derivation.
Upstream, only the two definitions matter: the fold that builds m2Num and the pattern-matching table explicitZ. No analytic estimates enter.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values at the fixed indices (0,0,2,1,2,1), so the kernel decision procedure checks integer equality and closes the goal. No lemmas beyond the unfoldings of m2Num and explicitZ are required.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the universal claim $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ by exhausting all Fin 4 cases. Each chunk equality such as this one is a leaf in that 4^6 case split (here the point with digits 0,0,2,1,2,1).
In the gravity stack this identity is bookkeeping infrastructure for the Regge midpoint M2/TT kernel certification: once every multi-index matches, the folded numerator may be replaced by the compact explicit table scaled by 8. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it is a finite combinatorial certificate inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.