e_203101
plain-language theorem explainer
For the six-index tuple (2,0,3,1,0,1) on Fin 4, the folded midpoint numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite it as one of the 256 kernel point-checks that assemble the global identity m2Num = 8·explicitZ. The proof is a single decide on concrete integers.
Claim. For indices $a=2$, $b=0$, $c=3$, $d=1$, $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 kernel integer $Z(a,b,c,d,i,j)$.
background
In the Regge exact-midpoint 4D analysis, the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each coupling term at a six-tuple of $\mathrm{Fin},4$ indices. The companion map $Z$ is an explicit integer-valued kernel on the same six indices, given by a finite case table (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$, and so on).
The module is chunk 8 of a 256-way partition of the kernel: each chunk discharges a block of concrete equalities $m_2^{\mathrm{num}}=8Z$ by computation, rather than by a symbolic closed form. The local setting is pure finite arithmetic over $\mathrm{Fin},4$ and $\mathbb{Z}$; no continuum limit or curvature hypothesis enters at this layer.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(2,0,3,1,0,1)$. The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $Z$ and multiplies by 8. Equality of the resulting integers is discharged by the kernel.
why it matters
Feeds the assembler 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$ and invocation of the chunk lemmas. That global identity is the certified algebraic core of the Regge exact-midpoint $M_2$ TT identity in 4D: it replaces an opaque summed coupling expression by an explicit sparse integer kernel, scaled by the universal factor 8.
Within Recognition gravity, this is bookkeeping infrastructure for the discrete curvature/midpoint calculus, not a forcing-chain step (T0–T8). It closes one cell of the 256-decide grid so the assembler can finish without sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.