e_211100
plain-language theorem explainer
For the six-index tuple (2,1,1,1,0,0) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one atomic cell in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=2$, $b=1$, $c=1$, $d=1$, $i=0$, $j=0$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(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 9 of a 256-cell kernel certification that the midpoint Regge numerator in 4D equals eight times a sparse explicit integer table. Indices run over $\mathrm{Fin},4$, matching the four spacetime directions of the discrete geometry.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a local contribution at each coupling triple for the six free indices. The comparison target $\mathrm{explicitZ}$ is a pattern-matched integer table on those same six indices (typical nonzero entries are $\pm 2$ or $4$).
The local claim is one concrete six-tuple evaluation inside that table identity, not the universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left-hand side by evaluating the fold of contributions at the fixed indices $(2,1,1,1,0,0)$, the right-hand side by looking up (or defaulting) the explicit kernel at those indices and multiplying by $8$. Lean’s decision procedure discharges the resulting integer equality.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states the identity for all six $\mathrm{Fin},4$ indices by exhaustive fin_cases and invokes each chunk cell such as this one. That universal equality is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT identity certification in the Gravity analysis stack.
In the Recognition framework this sits inside discrete gravity bookkeeping (Regge-type curvature and stress bookkeeping on a 4D lattice), downstream of the forcing chain’s $D=3$ spatial plus time structure. It does not itself touch $\phi$-ladder masses or $\alpha$; it only locks one numerator cell so the global midpoint identity can be cited without residual case obligations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.