e_033231

This module is chunk 3 of a 256-way kernel certification that the M₂ numerator equals eight times an explicit integer table Z on every sextuple of indices in $(\mathrm{Fin},4)^6$. The setting is the exact midpoint analysis of the 4D Regge TT identity in the Gravity stack.

The numerator is defined by folding a fixed coupling list: each term adds a contribution depending on the six indices, starting from 0. The explicit kernel Z is a pattern-matched integer table on the same six $\mathrm{Fin},4$ arguments (sample values include $4$, $-2$, and other small integers on the matched patterns).

Upstream, both maps live in the kernel certificate module; this chunk only discharges individual point equalities so a later assembler can quantify over all indices.

One-line computational proof: decide evaluates both sides at the concrete sextuple $(0,3,3,2,3,1)$. The left-hand side runs the fold that defines the numerator; the right-hand side multiplies the looked-up explicit Z value by 8. Equality of the resulting integers is discharged by the decision procedure. No lemmas beyond the two definitions are invoked.

The parent theorem is the full assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,,\mathrm{M}_2^{\mathrm{num}}=8Z$ and proves it by exhaustive fin_cases on all six indices. Each chunk theorem such as this one is a leaf of that case split.

In the Recognition gravity analysis, the identity certifies that the midpoint M₂ TT kernel collapses to a sparse explicit integer table, scaled by eight. That collapse is bookkeeping infrastructure for the exact discrete curvature identities used in the 4D Regge sector; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but it keeps the discrete gravity side machine-checked.