e_200302
plain-language theorem explainer
Case check that the Regge midpoint mass-squared numerator equals eight times the explicit integer kernel Z at multi-index (2,0,0,3,0,2) in (Fin 4)^6. Gravity analysts cite it as one of the 256 kernel decides in chunk 8 of the m2Num = 8·Z identity. The proof is a single decide on concrete integer values of both sides.
Claim. For indices $(a,b,c,d,i,j)=(2,0,0,3,0,2)$ with each entry in $\{0,1,2,3\}$, 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
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each term's contribution at the given multi-index. The comparison target is an explicit piecewise integer table $Z$ (pattern-matched on the six indices), recording the closed-form midpoint coupling.
The local module is chunk 8 of the identity $m_2^{\mathrm{num}}=8\cdot Z$. The full statement ranges over all $4^6$ index tuples; this file discharges a block of those tuples by kernel decides. Upstream, $m_2^{\mathrm{num}}$ and $Z$ are pure definitions in the kernel certificate module, with no analytic hypotheses.
proof idea
One-line computational proof: decide evaluates both sides at the concrete multi-index $(2,0,0,3,0,2)$. The left side runs the fold that defines the numerator; the right side looks up (or defaults) the explicit $Z$ table and multiplies by 8. Equality of the resulting integers is decided in the kernel, with no lemmas or rewriting.
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 the six Fin-4 indices. Each chunk theorem such as this one closes one generated goal, so the global midpoint identity is only as strong as the full set of decides.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge mass-squared coupling in 4D, not a forcing-chain step (T0–T8). It does not touch $\phi$, the eight-tick octave, or the $\alpha$ band; it is pure discrete kernel certification supporting later continuum or continuum-limit claims that quote the assembled equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.