e_320221
plain-language theorem explainer
Pointwise identity: the Regge midpoint m2 numerator at multi-index (3,2,0,2,2,1) equals eight times the explicit kernel Z there. Gravity analysts cite it as one cell of the 4D TT-identity kernel table. The proof is a single kernel decide on closed integer arithmetic.
Claim. For indices $(a,b,c,d,i,j)=(3,2,0,2,2,1)$ with each index in $\{0,1,2,3\}$, the folded coupling 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
This module is chunk 14 of the finite case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the full $(\mathrm{Fin},4)^6$ grid for the 4D Regge exact-midpoint TT identity.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of a fixed coupling list: sum the local contributions of each coupling term at those six indices. The explicit kernel $Z$ is a sparse integer lookup on the same six $\mathrm{Fin},4$ arguments (nonzero only on a short list of index patterns, with values such as $4$ or $-2$).
Both objects live in the kernel-certificate module imported here; the chunk modules only discharge individual grid points.
proof idea
One-line computational proof: decide evaluates both sides as concrete integers (the fold defining the numerator versus eight times the matched $Z$ clause) and closes the equality by kernel reduction. No lemmas are invoked beyond the definitions of the two sides.
why it matters
Feeds the assembly theorem $m_2^{\mathrm{num}}=8\cdot Z$ for all six $\mathrm{Fin},4$ indices, which is proved by exhaustive fin_cases and consumes one decide per grid point (this declaration is the cell $(3,2,0,2,2,1)$). That global identity is the algebraic core of the 4D Regge exact-midpoint M2 TT certificate in the Gravity analysis stack. It does not itself touch the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete curvature bookkeeping needed before continuum or phenomenological gravity claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.