e_010213
plain-language theorem explainer
Kernel equality for one sextuple of Fin-4 indices: the folded Regge midpoint numerator m2Num at (0,1,0,2,1,3) equals eight times the explicit integer table entry Z at those indices. Gravity analysts cite it only as a case in the full 4D midpoint identity assembly. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,2,1,3)$ 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 one chunk of the 4D Regge exact-midpoint $M_2$ TT-identity certification. The local claim is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a block of the $4^6=4096$ index sextuples, discharged by kernel decides.
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a contribution functional at those indices. The companion table $Z$ is an explicit piecewise integer function on $(\mathbb{F}_4)^6$ (sample clauses return $4$, $-2$, etc.). Both live in the kernel-cert module imported here.
The present declaration fixes one concrete sextuple $(0,1,0,2,1,3)$ inside chunk 1.
proof idea
One-line computational proof: decide. After the six Fin-4 arguments are substituted, both sides reduce to concrete integers (the fold for the numerator versus eight times the matching clause of the explicit table), and the kernel decision procedure checks equality.
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$ by exhaustive fin_cases over all six indices and invokes the chunk lemmas as cases. That global identity is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT certification in the Gravity analysis stack. It is bookkeeping inside discrete gravity, not a forcing-chain (T0–T8) step, but it underwrites the continuum-limit identities used downstream in the RS gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.