e_300032
plain-language theorem explainer
Single kernel identity: the Regge midpoint mass-squared numerator at multi-index (3,0,0,0,3,2) equals eight times the explicit Z-table entry there. Gravity analysts cite it only as one of the 256 finite-case checks that assemble the global m2Num = 8·explicitZ identity. The proof is a pure kernel decision (`decide`).
Claim. For indices $(a,b,c,d,i,j)=(3,0,0,0,3,2)$ in $(\mathbb{F}_4)^6$, 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
This module is chunk 12 of a 256-way case split proving that the four-dimensional Regge midpoint mass-squared numerator coincides with eight times a hand-tabulated integer kernel. The ambient setting is exact midpoint analysis for a discrete gravity / Regge-calculus identity in 4D.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at the six $\mathbb{F}_4$ indices. The comparison object $Z$ is an explicit pattern-matched integer table on $(\mathbb{F}_4)^6$ (sample clauses include values $4$, $-2$, and so on). Both live in the kernel certificate module imported here.
The global claim is $\forall$ indices, $m_2^{\mathrm{num}}=8Z$. Because the domain is finite of size $4^6=4096$ but the effective kernel is organized into 256 decide-able points, the development splits into named point lemmas such as this one.
proof idea
One-line computational proof: decide. Lean reduces both sides of the integer equality (the fold that defines the numerator at $(3,0,0,0,3,2)$, and eight times the matching explicitZ clause) to concrete Int values and checks equality in the kernel. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8Z$ and discharges it by exhaustive fin_cases on the six $\mathbb{F}_4$ indices. Each chunk lemma such as this one is a named, machine-checked cell of that case tree (module doc: "m2Num = 8·explicitZ, chunk 12 (256 kernel decides)").
In the Recognition gravity stack this identity is bookkeeping infrastructure for the exact midpoint Regge analysis: it certifies that the folded coupling numerator is a pure multiple of the explicit kernel table, so later curvature or mass-squared identities can quote the closed table instead of re-folding. It does not itself touch the T0–T8 forcing chain, $\phi$-ladder masses, or the $\alpha$ band; it is local to the 4D Regge midpoint certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.