e_022012
plain-language theorem explainer
For the six-index tuple (0,2,2,0,1,2) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel decides that assemble the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=2$, $c=2$, $d=0$, $i=1$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a 256-case kernel certification that the Regge exact-midpoint numerator equals eight times a closed-form integer table. The ambient setting is 4D discrete gravity analysis: six indices in $\mathrm{Fin},4$ label a pair of edge/face slots in the midpoint coupling.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list and summing a local contribution at each term. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by an exhaustive pattern table (typical nonzero entries are $\pm 2$ or $4$).
The global claim is that these two agree up to the universal factor 8 for every index sextuple. Each chunk theorem pins one concrete sextuple so the assembler can discharge the universal statement by fin_cases.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the six Fin 4 arguments are literals, so the equality is a pure integer decision with no lemmas beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases over all six indices, invoking one decide per cell. Without the chunk cells, that universal identity has no certified base.
In the Recognition gravity stack this identity is bookkeeping for the Regge exact-midpoint $M_2$ TT sector in 4D: it replaces a folded coupling sum by a sparse closed-form kernel, which is what later curvature and continuum-limit arguments actually consume. It is pure discrete-kernel algebra, not a continuum GR theorem, and does not by itself force $D=3$ or the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.