e_020200
plain-language theorem explainer
Pointwise check that the Regge midpoint numerator m2Num at multi-index (0,2,0,2,0,0) equals eight times the explicit integer table explicitZ at the same indices. Gravity analysts cite it as one of the 256 kernel cells assembled into the global identity m2Num = 8·explicitZ. The proof is a single kernel decide on concrete Fin-4 data.
Claim. For indices $a=0$, $b=2$, $c=0$, $d=2$, $i=0$, $j=0$ in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit closed-form integer at those indices: $\mathrm{num}(0,2,0,2,0,0)=8\,Z(0,2,0,2,0,0)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices are compared. The numerator is obtained by folding a fixed coupling list: each term contributes an integer depending on the six indices, and the fold starts from zero. The comparison target is an explicit piecewise table $Z$ on the same index domain, with values such as $\pm 2,,4$ on selected patterns and (implicitly) zero elsewhere.
This module is chunk 2 of the 256-cell kernel that discharges the pointwise identity numerator $= 8Z$. The local setting is pure finite enumeration: every sextuple of $\mathrm{Fin},4$ indices is a concrete small integer problem, not an analytic continuum argument.
Upstream, the two maps are the certified kernel definitions of the numerator fold and the explicit table; no further analytic hypotheses are required for a single cell.
proof idea
One-line computational proof: decide evaluates both sides on the fixed sextuple $(0,2,0,2,0,0)$ and confirms integer equality. No lemmas beyond the kernel definitions of the numerator fold and the explicit table are invoked; the tactic closes the goal because both expressions reduce to concrete Int values.
why it matters
The parent assembly theorem states $\forall a,b,c,d,i,j:\mathrm{Fin},4$, numerator $= 8Z$, and proves it by six nested fin_cases over the index domain. Each cell such as this one supplies one branch of that case split. Without the full 256-cell cover, the global algebraic identity used in the Regge midpoint $M_2$ TT analysis would remain open.
In the Recognition gravity stack this identity is bookkeeping infrastructure: it certifies that a folded coupling expression collapses to a sparse explicit integer kernel, which is the form needed for later exact midpoint and deficit identities. It does not itself invoke the forcing chain (T5–T8), RCL, or the $\varphi$-ladder; it is a finite combinatorial lemma inside the 4D Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.