e_021103
plain-language theorem explainer
For the six-tuple of Fin-4 indices (0,2,1,1,0,3), the folded Regge midpoint numerator equals eight times the explicit integer kernel. Gravity analysts building the 4D midpoint M2TT identity cite these per-cell checks when assembling the global equality. The proof is a single computational decide on the two concrete integers.
Claim. For indices $a=0$, $b=2$, $c=1$, $d=1$, $i=0$, $j=3$ ranging in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel value: $m_2^{\mathrm{num}}(0,2,1,1,0,3)=8\,Z_{\mathrm{expl}}(0,2,1,1,0,3)$.
background
This module is one chunk of the kernel certification that the 4D Regge midpoint numerator coincides with eight times an explicit integer table. The local slogan is "$m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$, chunk 2 (256 kernel decides)."
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add a contribution for each coupling term evaluated at the six Fin-4 indices. The explicit kernel $Z_{\mathrm{expl}}$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on for particular index patterns).
Both objects live in the Gravity analysis layer that certifies exact midpoint identities for the discrete Regge curvature side of Recognition Science gravity.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(0,2,1,1,0,3)$ and checks integer equality. The left side runs the fold that defines the numerator; the right side multiplies the table lookup by eight. No lemmas are invoked beyond the definitions of the numerator and the explicit kernel.
why it matters
This cell is one of the $4^6$ concrete equalities that the assembler theorem m2Num_eq_eight_explicitZ glues into the universal statement
$$\forall a,b,c,d,i,j:\mathrm{Fin},4,\quad m_2^{\mathrm{num}}(a,b,c,d,i,j)=8,Z_{\mathrm{expl}}(a,b,c,d,i,j).$$
That assembler proceeds by exhaustive fin_cases on the six indices and lands on chunk theorems such as this one. In the broader RS gravity stack, the identity underwrites exact midpoint M2TT bookkeeping for the discrete curvature kernel, so downstream continuum or continuum-limit arguments can treat the numerator as a pure multiple of the tabulated kernel rather than an opaque fold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.