e_200203
plain-language theorem explainer
Pointwise integer identity: the Regge midpoint m2 numerator at multi-index (2,0,0,2,0,3) equals eight times the explicit Z kernel at those same Fin-4 indices. Gravity analysts cite it as one cell of the 4D TT midpoint certification. The proof is a single kernel decide on a closed integer equality.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,0,0,2,0,3)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $m_2(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 8 of a finite kernel certification that the 4D Regge-midpoint $m_2$ numerator agrees with eight times a tabulated integer kernel on every sextuple of $\mathrm{Fin},4$ indices (256 decides per chunk).
Upstream, $m_2$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling entry at the six indices. The explicit kernel $Z$ is a piecewise $\mathbb{Z}$-valued table on $(\mathrm{Fin},4)^6$, with sample values such as $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$.
The local goal is purely algebraic: evaluate both sides at one concrete multi-index and check equality in $\mathbb{Z}$. No continuum or variational content is invoked at this layer.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six indices are fixed literals, so Lean's decision procedure discharges the equality with no lemmas, rewrites, or case splits inside this declaration.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2=8Z$ and proves it by exhaustive fin_cases on the six $\mathrm{Fin},4$ arguments. Each chunk cell such as this one supplies a closed decide for one sextuple so the global identity is a finite certificate rather than an abstract rewrite.
In the Gravity analysis stack this underwrites the exact midpoint M2 tensor-tensor identity in 4D Regge calculus: the numerator side of the discrete curvature/coupling expression matches the explicit kernel used downstream. It is bookkeeping inside the discrete-gravity certification, not a forcing-chain (T0–T8) step, but it is required before continuum or phenomenological gravity claims can rest on that kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.