e_201220
plain-language theorem explainer
Pointwise identity: the midpoint Regge m₂ numerator at multi-index (2,0,1,2,2,0) equals eight times the explicit kernel Z there. Gravity analysts cite it as one cell of the 4D TT mass-squared kernel table. The proof is a single kernel decide on concrete Fin-4 integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,1,2,2,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 8 of a 256-way split of the 4D Regge exact-midpoint identity $m_2=8Z$ on the TT sector. Indices run over $\mathrm{Fin},4$, matching a discrete 4-simplex / edge-label bookkeeping for the midpoint scheme.
Upstream, $m_2$ (written m2Num) is the integer obtained by folding a fixed coupling list and summing each term's contribution at the six indices. The comparison target $Z$ (written explicitZ) is a closed-form case table $\mathrm{Fin},4^6\to\mathbb{Z}$ listing the nonzero kernel entries (e.g. $4$, $-2$, and symmetric permutations).
Local goal of the chunk: discharge one concrete sextuple by computation so the assembler can rebuild the full quantified statement without re-deriving the fold.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are literals, so the kernel evaluates the fold that defines the numerator and the matching clause of the explicit $Z$ table and checks equality in $\mathbb{Z}$. No algebraic lemmas are invoked beyond that decision procedure.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall(a,b,c,d,i,j),,m_2=8Z$ by exhausting all $\mathrm{Fin},4$ cases. That universal identity is the algebraic core of the 4D Regge exact-midpoint M₂ TT kernel certificate in the Gravity analysis stack.
In the broader Recognition framework this sits inside the discrete-gravity / Regge route to the continuum limit, not on the T0–T8 forcing chain itself. It is bookkeeping infrastructure: once every chunk cell is decided, the midpoint mass-squared numerator is certified equal to eight times the explicit kernel, clearing a gate for later continuum or phenomenological gravity claims. No open scaffold remains at this cell; the only residual risk is inconsistency among sibling chunks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.