e_002000
plain-language theorem explainer
Pointwise identity: the Regge midpoint mass-squared numerator at multi-index (0,0,2,0,0,0) equals eight times the explicit kernel Z there. Gravity analysts cite it as one of 256 kernel cells that assemble the global m2Num = 8·explicitZ theorem. The proof is a single decidability check on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,0,2,0,0,0)$ in $(\mathbb{F}_4)^6$, the midpoint mass-squared 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 0 of a 256-cell kernel that certifies $m_2^{\mathrm{num}}=8\cdot Z$ on every 6-tuple of indices in $\mathbb{F}_4$. The setting is 4D Regge calculus at the exact midpoint: discrete curvature couplings are reduced to integer arithmetic so the identity can be machine-checked.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution contrib t a b c d i j. The comparison target explicitZ is a closed-form integer table on $(\mathbb{F}_4)^6$ (sample values include $4$, $-2$, and $0$ on unspecified patterns). Both live in the KernelCert module imported here.
The present declaration fixes one concrete cell, $(0,0,2,0,0,0)$, rather than quantifying over all indices.
proof idea
One-line computational proof: by decide. Lean evaluates both sides at the fixed multi-index to concrete Int values and discharges equality by the decidable instance on integers. No algebraic lemmas are invoked; the kernel cell is pure evaluation.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ and is proved by exhaustive fin_cases on all six $\mathbb{F}_4$ indices, each case landing on a chunk identity of this form.
In the gravity analysis stack, that global identity is the certified bridge between the folded coupling definition of the midpoint mass-squared numerator and the explicit kernel used downstream. It is bookkeeping infrastructure for the Regge midpoint $M^2$ TT identity in 4D, not a new physical law: once every cell matches, the analytic side may quote a single clean equality instead of a fold.
No forcing-chain landmark (T5–T8, RCL, $\varphi$) is touched directly; the result is local to the discrete gravity kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.