e_210331
plain-language theorem explainer
At multi-index (2,1,0,3,3,1), the Regge midpoint m₂ numerator equals eight times the explicit Z table entry. Gravity analysts cite this as one of 256 kernel point checks that assemble into the global m₂Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,1,0,3,3,1)$ with each coordinate in $\{0,1,2,3\}$, the integer $m_2$ numerator equals $8$ times the explicit $Z$ value at those indices: $m_2(2,1,0,3,3,1)=8\,Z(2,1,0,3,3,1)$.
background
This module is chunk 9 of a 256-way case split proving that the Regge midpoint $m_2$ numerator coincides with eight times a closed-form integer table on $(\mathrm{Fin},4)^6$. The local setting is pure integer arithmetic on coupling contributions; no continuum limit is taken here.
The numerator $m_2(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six indices. The explicit table $Z$ is a pattern-matched integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
Both definitions live in the kernel certificate module imported by this chunk. The identity $m_2=8Z$ is the algebraic content being certified pointwise before assembly.
proof idea
One-line kernel proof: decide evaluates both sides at the concrete indices $(2,1,0,3,3,1)$ and checks integer equality. No lemmas are invoked; the fold defining the numerator and the pattern match defining $Z$ reduce to numerals that Lean’s decision procedure compares.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2=8Z$ and discharges the claim by exhaustive fin_cases on all six indices. Each chunk such as this one pins a single lattice point so the global identity is a finite conjunction of kernel facts rather than an opaque tactic script.
In the Recognition gravity stack this identity is bookkeeping for the exact midpoint Regge $m_2$ tensor structure in 4D: once numerator and table agree everywhere, downstream curvature and continuum-matching arguments can quote the closed form $Z$ instead of the fold. It does not itself touch the forcing chain (T0–T8), $\phi$, or the eight-tick octave; it is infrastructure inside the discrete gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.