e_010000
plain-language theorem explainer
For the six Fin-4 indices (0,1,0,0,0,0), the midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one atomic case in the 256-point kernel identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}1$, $c{=}0$, $d{=}0$, $i{=}0$, $j{=}0$ in $\mathrm{Fin}\,4$, the folded midpoint numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-case kernel certification that the Regge midpoint numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, matching a 4D discrete geometry setting.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a coupling list and summing a local contribution at each tuple $(a,b,c,d,i,j)$. The comparison target $\mathrm{explicitZ}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern match (nonzero only on a sparse set of index patterns, with values such as $4$ and $-2$).
The global claim assembled downstream is that $m_2^{\mathrm{num}}=8\cdot\mathrm{explicitZ}$ at every index sextuple. Each chunk theorem discharges one concrete sextuple by computation.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,1,0,0,0,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of $m_2^{\mathrm{num}}$ (fold of contributions) and $\mathrm{explicitZ}$ (pattern table).
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which introduces all six $\mathrm{Fin},4$ indices and splits by fin_cases, routing each leaf to a chunk theorem of this form. That universal identity is the certified algebraic core of the 4D Regge exact-midpoint $M_2$ TT analysis in the Gravity domain.
Within Recognition Science gravity work, such kernel equalities underwrite discrete curvature bookkeeping on the eight-tick / $D=3$ side of the forcing chain only indirectly: they secure the 4D combinatorial identity used by the midpoint mass/curvature numerics, not a T0–T8 step itself. Closing all 256 decides removes scaffolding from the midpoint identity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.