e_023313
plain-language theorem explainer
For the single multi-index $(0,2,3,3,1,3)$ on $\mathrm{Fin}\,4$, the folded Regge numerator $m_2^{\mathrm{num}}$ equals eight times the explicit kernel value $Z$. Gravity analysts cite it as one atomic cell in the 4D midpoint $M_2$ TT identity. The proof is a pure kernel decision: Lean evaluates both integer sides and checks equality.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$ with $(a,b,c,d,i,j)=(0,2,3,3,1,3)$. Write $m_2^{\mathrm{num}}$ for the integer obtained by folding the coupling list of local contributions, and $Z_{\mathrm{ex}}$ for the explicit piecewise integer kernel. Then $m_2^{\mathrm{num}}(0,2,3,3,1,3)=8\,Z_{\mathrm{ex}}(0,2,3,3,1,3)$.
background
This module is one chunk of the 4D Regge midpoint analysis that certifies the numerator identity $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{ex}}$ by exhaustive kernel decisions (256 cells in the present chunk family). Indices run over $\mathrm{Fin},4$, matching the four discrete directions of the 4-simplex edge data.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start from $0$ and add each local contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z_{\mathrm{ex}}$ is an explicit integer-valued function on six $\mathrm{Fin},4$ arguments, tabulated by pattern (e.g. $(0,0,1,1,2,2)\mapsto 4$, $(0,0,1,2,1,2)\mapsto -2$).
The surrounding Gravity.Analysis development assembles these pointwise equalities into a single universal statement over all index sextuples.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six concrete $\mathrm{Fin},4$ indices are substituted, so the kernel reduces $m_2^{\mathrm{num}},0,2,3,3,1,3$ and $8\cdot Z_{\mathrm{ex}},0,2,3,3,1,3$ to numerals and checks equality. No lemmas beyond the definitions of $m_2^{\mathrm{num}}$ and $Z_{\mathrm{ex}}$ are required.
why it matters
The parent theorem $m_2^{\mathrm{num}}=8,Z_{\mathrm{ex}}$ (all $a,b,c,d,i,j\in\mathrm{Fin},4$) is proved by six nested fin_cases sweeps; each leaf is exactly one of these chunk cells. The present declaration discharges the leaf $(0,2,3,3,1,3)$.
In the Recognition gravity stack this identity is part of the exact midpoint $M_2$ TT analysis in 4D Regge calculus: it converts a folded coupling sum into a sparse closed kernel, which is the algebraic input needed for later continuum and continuum-limit comparisons. It does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it sits inside the discrete-gravity layer those continuum claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.