e_030123
plain-language theorem explainer
Concrete index identity: the midpoint M2 numerator at the Fin-4 sextuple (0,3,0,1,2,3) equals eight times the explicit Z kernel entry. Gravity analysts assembling the 4D Regge midpoint M2=8Z certificate cite it as one of the 256 decided cells. The proof is a single kernel `decide` on fully concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,0,1,2,3)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(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 3 of a 256-cell case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all of $(\mathrm{Fin},4)^6$ in the 4D Regge exact-midpoint analysis. The ambient setting is discrete gravity: edge couplings on a 4-simplex skeleton, with a closed-form kernel $Z$ and a folded numerator built from a fixed coupling list.
Upstream, m2Num a b c d i j is the integer obtained by folding couplingZList with a local contribution contrib at those six indices. explicitZ is the sparse lookup table of intended kernel values (e.g. $4$, $-2$, and zeros off the listed patterns). The identity claimed here is one concrete cell of that table versus the fold.
The parent assembly theorem quantifies over every sextuple by fin_cases, so each chunk theorem discharges one numeric obligation the kernel can decide.
proof idea
One-line proof: by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel evaluates the fold defining the numerator and the pattern-match defining explicit $Z$, then checks equality. No lemmas are invoked beyond definitional reduction.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8\cdot Z$ and proves it by exhaustive fin_cases on the six indices. That universal identity is the algebraic core of the Regge exact-midpoint M2/TT certificate in 4D: it converts the folded coupling expression into the closed explicit kernel used downstream in the gravity analysis stack.
Within Recognition Science gravity work, this is bookkeeping infrastructure rather than a forcing-chain landmark (T5–T8). It closes one cell of the finite case matrix so the midpoint curvature identity can be cited without residual numeric gaps. Sibling chunk theorems cover the other sextuples in the same style.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.