e_201322
plain-language theorem explainer
Pointwise identity: the Regge midpoint numerator coupling at multi-index (2,0,1,3,2,2) equals eight times the explicit kernel value Z at those indices. Gravity analysts cite it when assembling the full 4D m2Num = 8·explicitZ certificate. The proof is a single kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,0,1,3,2,2)$ in $\mathrm{Fin}\,4$, the folded numerator coupling $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 one chunk of the 4D Regge exact-midpoint M2TT identity certification: the claim that the numerator coupling sum equals eight times a closed-form kernel on every six-tuple of $\mathrm{Fin},4$ indices (256 cases, split across chunks).
Upstream, $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list, yielding an integer for each multi-index. The explicit kernel $Z$ is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and so on). The local setting is pure integer arithmetic on those tables, not continuum GR.
proof idea
One-line decide proof. Both sides evaluate to concrete integers once the six indices are fixed, so the kernel closes the equality with no lemmas beyond the definitions of the numerator fold and the explicit $Z$ table.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall$ six-tuples $m_2^{\mathrm{num}}=8Z$ and discharges the claim by exhaustive fin_cases on each coordinate, invoking one chunk theorem per cell. This chunk (module doc: chunk 8) is one of those cells. In the gravity stack it is bookkeeping for the exact midpoint M2TT identity in 4D Regge analysis, not a new physical law; it locks the discrete kernel so later continuum or continuum-limit arguments can quote a fully certified algebraic identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.