e_122201
plain-language theorem explainer
For the six-index slot (1,2,2,2,0,1) on Fin 4, the folded Regge midpoint numerator equals eight times the closed-form kernel value. Gravity analysts cite it when assembling the full 4D m2Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $a{=}1,b{=}2,c{=}2,d{=}2,i{=}0,j{=}1$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z_{\mathrm{explicit}}(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-case kernel certification that the 4D Regge exact-midpoint numerator matches eight times a closed-form table. The ambient setting is discrete gravity analysis: edge and hinge couplings on a 4-simplex lattice with Fin-4 labels.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing each contribution at the six indices. The comparison object $Z_{\mathrm{explicit}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern match (nonzero only on a sparse set of index patterns, e.g. values $\pm 2,4$).
The local claim is one concrete cell of that table equality, not the universal statement.
proof idea
One-line kernel proof: decide evaluates both sides as concrete integers (the fold for $m_2^{\mathrm{num}}$ at $(1,2,2,2,0,1)$ and $8\cdot Z_{\mathrm{explicit}}$ at the same point) and discharges propositional equality by computation. No lemmas beyond the two definitions are invoked.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8,Z_{\mathrm{explicit}}$ and proves it by exhaustive fin_cases on all six Fin-4 arguments, invoking one cell theorem per case. This declaration is the cell for $(1,2,2,2,0,1)$.
In the Recognition gravity stack the identity certifies that the midpoint TT numerator on the 4D Regge complex collapses to a sparse explicit kernel, a computational prerequisite for later continuum or continuum-limit comparisons. It does not itself touch T0–T8 or the J-cost forcing chain; it is pure discrete-gravity bookkeeping inside the Gravity.Analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.