e_020221
plain-language theorem explainer
At multi-index (0,2,0,2,2,1), the folded Regge midpoint mass-squared numerator equals eight times the explicit integer Z-kernel. Gravity analysts cite it as one of the 256 concrete kernel checks that assemble the full 4D identity. The proof is a single native decide on both integer sides.
Claim. For indices $(a,b,c,d,i,j)=(0,2,0,2,2,1)$ in $(\mathrm{Fin}\,4)^6$, 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 2 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on every 4D multi-index. The setting is the exact midpoint Regge analysis for the transverse-traceless sector in four dimensions.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution at the six Fin-4 slots. The explicit kernel $Z$ is a closed integer table on those same six indices (typical nonzero values $\pm 2,,4$ on the matched patterns).
Upstream, both definitions live in the kernel certificate module; this chunk only evaluates one concrete point of the claimed scalar identity.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,2,0,2,2,1)$. The left side runs the fold that defines the numerator; the right side looks up (or defaults) the explicit $Z$ entry and multiplies by 8. Equality of the resulting integers is discharged by the kernel decision procedure. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem m2Num_eq_eight_explicitZ assembles every Fin-4 case by nested fin_cases and dispatches each leaf to a chunk identity of this form. Without the pointwise checks, the global numerator-to-kernel relation used in the 4D midpoint Regge TT identity does not close.
In the Recognition gravity stack this is pure algebraic certification of the discrete curvature coupling bookkeeping, not a new physical law. It sits downstream of the kernel table and upstream of the assembled identity that later feeds continuum or continuum-limit comparisons. No T0–T8 forcing step is touched; the landmark relevance is only that the 4D Regge sector stays exactly certified once all 256 chunks succeed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.