e_012012
plain-language theorem explainer
Pointwise identity: the folded midpoint M2 numerator at index tuple (0,1,2,0,1,2) equals eight times the explicit Z-table entry at those same indices. Gravity analysts assembling the 4D Regge midpoint TT kernel cite it as one of 256 decide-chunks. Proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,0,1,2)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, the TT-sector mass-squared numerator is built by folding a fixed coupling list: each term contributes an integer depending on six $\mathrm{Fin},4$ indices, and $m_2^{\mathrm{num}}$ is that fold sum. Parallel to it sits an explicit sparse table $Z$ on the same six indices, with only a handful of nonzero pattern-matched values (e.g. $\pm 2,,4$).
The local module is chunk 1 of a 256-way case split whose sole job is to certify $m_2^{\mathrm{num}}=8Z$ at every concrete index tuple. Upstream, both $m_2^{\mathrm{num}}$ and $Z$ are pure definitions in the kernel-cert module; no analytic hypothesis is left open at this layer.
proof idea
One-line closed proof: decide. Both sides reduce to concrete Int values (the fold over the coupling list versus eight times the matched table entry), so the kernel discharges equality with no lemmas or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for all six $\mathrm{Fin},4$ indices by exhaustive fin_cases and invokes each chunk such as this one. That global equality is the algebraic backbone of the exact midpoint M2 TT identity in 4D Regge gravity inside the Recognition stack: once numerator and explicit $Z$ match up to the factor 8, downstream curvature and continuum-limit arguments can quote a closed integer formula rather than an opaque fold. No forcing-chain landmark (T5–T8) is touched directly; this is pure discrete-gravity bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.