e_303202
plain-language theorem explainer
For the Fin-4 six-tuple (3,0,3,2,0,2), the folded M2 numerator equals eight times the explicit integer Z-kernel entry. Gravity analysts assembling the 4D Regge midpoint M2–TT identity cite this as one pointwise kernel case among 256. The proof is a single computational decide on both integer sides.
Claim. For indices $a=3$, $b=0$, $c=3$, $d=2$, $i=0$, $j=2$ in $\mathbb{F}_4$, the M2 numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge-exact midpoint analysis, the M2 numerator is an integer obtained by folding a fixed list of coupling contributions over six indices in $\mathbb{F}_4$. The explicit Z kernel is a closed-form case table on the same six indices, returning small integers (typically $\pm 2$ or $\pm 4$ on the listed patterns).
This module is chunk 12 of the 256 kernel decides that establish the pointwise relation numerator $= 8\cdot Z$ on every multi-index. Upstream, the two sides are pure definitions: the fold of contributions versus the pattern-matched table. The parent assembly theorem then quantifies over all of $\mathbb{F}_4^6$.
proof idea
Both sides evaluate to concrete integers once the six indices are fixed. The proof is a one-line decide: Lean computes the fold that defines the numerator and the case match that defines the explicit kernel, then checks numerical equality. No intermediate lemmas are applied beyond unfolding those two definitions.
why it matters
This case is one brick in the universal equality that the M2 numerator equals eight times the explicit Z kernel for every six-tuple in $\mathbb{F}_4$. Downstream, the assembly theorem packages all Fin-4 cases (via exhaustive case split) into that single quantified identity, which is the algebraic content of the Regge-exact midpoint M2–TT relation in four dimensions.
Within Recognition Science this sits in the discrete gravity analysis layer, not in the T0–T8 forcing chain or the J-cost uniqueness step. It closes one computational obligation on the path from the kernel certificate to the assembled midpoint identity used by later gravity results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.