e_201333
plain-language theorem explainer
For the six-index tuple (2,0,1,3,3,3) on Fin 4, the folded Regge midpoint numerator equals eight times the closed-form kernel value. Gravity analysts cite it when assembling the pointwise identity m2Num = 8·explicitZ over the full 4^6 grid. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a{=}2,\,b{=}0,\,c{=}1,\,d{=}3,\,i{=}3,\,j{=}3$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(2,0,1,3,3,3)$ equals $8$ times the explicit kernel integer $Z(2,0,1,3,3,3)$.
background
In the 4D Regge exact-midpoint analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer depending on six Fin-4 indices $(a,b,c,d,i,j)$. The companion map $Z_{\mathrm{explicit}}$ is a sparse pattern-matched integer table on the same index domain (typical nonzero values $\pm 2,,4$).
The local module is one of several decide-chunks whose sole job is to check $m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ at concrete points. Module doc: "m2Num = 8·explicitZ, chunk 8 (256 kernel decides)." Upstream, both sides are pure defs in the KernelCert module; no analytic hypotheses are required beyond the integer arithmetic of those defs.
proof idea
One-line kernel proof: by decide. Lean reduces both m2Num 2 0 1 3 3 3 (the fold of contrib over couplingZList) and 8 * explicitZ 2 0 1 3 3 3 (lookup in the pattern table, scaled) to concrete integers and checks equality by computation. No lemmas are invoked beyond the two defs.
why it matters
This pointwise certificate is consumed by the assembler m2Num_eq_eight_explicitZ, which states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and discharges it by exhaustive fin_cases on all six Fin-4 indices. The chunk therefore closes one cell of the $4^6$ case tree that underwrites the exact midpoint $M_2$ TT identity in 4D Regge calculus.
Within Recognition gravity, that identity is bookkeeping for the discrete curvature/coupling kernel, not a forcing-chain step (T0–T8). It sits downstream of the KernelCert tables and upstream of any theorem that quotes the assembled eight-factor relation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.