e_213111
plain-language theorem explainer
Pointwise identity: the midpoint M2 numerator at index sextuple (2,1,3,1,1,1) equals eight times the explicit kernel Z there. Gravity analysts assembling the 4D Regge midpoint M2=8Z certificate cite this kernel cell. Proof is a single kernel `decide` on concrete integer arithmetic.
Claim. For the discrete index sextuple $(a,b,c,d,i,j)=(2,1,3,1,1,1)$ with each index in $\{0,1,2,3\}$, the midpoint $M_2$ numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(2,1,3,1,1,1)=8\,Z(2,1,3,1,1,1)$.
background
This module is chunk 9 of a finite case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on the full $4^6$ index space of the 4D Regge exact-midpoint TT identity. Indices run in $\mathrm{Fin},4$ (values $0..3$).
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at those six indices. The comparison target $\mathrm{explicitZ}$ is a closed-form integer kernel on the same six indices (pattern-matched constants such as $4$, $-2$, and so on).
The local claim is one concrete cell of that equality, not the quantified statement.
proof idea
One-line kernel proof: decide. Both sides reduce to closed integer expressions once the six Fin 4 arguments are literals, so the decision procedure checks equality of two concrete Int values 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,Z$ and discharges the universal goal by exhaustive fin_cases over the six indices. Chunk theorems like this one supply (or mirror) the per-cell facts that make the 4D midpoint M2–TT kernel identity fully computational.
In the gravity analysis stack this is bookkeeping infrastructure for the Regge exact-midpoint certificate, not a dynamical law. It does not itself invoke Recognition landmarks (T5–T8, RCL, $\varphi$), but it hardens a discrete identity used downstream in the RS gravity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.