e_233223
plain-language theorem explainer
For the six-index tuple (2,3,3,2,2,3) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one atomic cell in the 4D Regge exact-midpoint identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}2,b{=}3,c{=}3,d{=}2,i{=}2,j{=}3$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8\,Z(a,b,c,d,i,j)$, where $Z$ is the explicit integer kernel and $m_2^{\mathrm{num}}$ is the fold of coupling contributions.
background
This module is chunk 11 of a 256-cell kernel certification that the 4D Regge exact-midpoint numerator equals eight times a closed-form integer table. Indices run over $\mathrm{Fin},4$, labeling discrete spacetime directions in the Regge calculus setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term evaluated at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six indices (typical values $\pm 2,\pm 4$, and zero off the listed patterns).
The local claim is the equality at one concrete sextuple. Sibling theorems cover the other cells; the assemble theorem glues them into a universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values: the left by evaluating the fold of contributions at $(2,3,3,2,2,3)$, the right by looking up explicitZ at those indices and multiplying by 8. Lean’s kernel decision procedure checks integer equality; no lemmas beyond the two definitions are invoked.
why it matters
Feeds the assemble theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases over $\mathrm{Fin},4^6$. That identity is the certified algebraic core of the 4D Regge exact-midpoint $M_2$ TT analysis in the Gravity domain.
In the Recognition framework this sits inside discrete gravity bookkeeping (Regge calculus on the recognition lattice), not the T0–T8 forcing chain itself. It closes one of 256 decide cells so the universal equality is free of sorry and free of hidden hypotheses. Downstream curvature and continuum-limit arguments can quote the assembled identity rather than re-expanding the fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.