e_102023

This module is chunk 4 of a 256-case kernel certification that the 4D Regge midpoint numerator agrees with an explicit integer table, scaled by eight. The ambient setting is discrete gravity analysis: curvature and stress-energy contributions on a 4-simplex lattice are reduced to finite integer identities on index tuples in $(\mathrm{Fin},4)^6$.

The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at 0 and add each contribution term evaluated at the six indices. The comparison table $Z_{\mathrm{expl}}$ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by pattern-matching clauses (for example $(0,0,1,1,2,2)\mapsto 4$ and several sign-flipped off-diagonal patterns $\mapsto -2$).

The local claim is only the equality at one concrete six-tuple; the sibling theorems cover the rest of the chunk.

One-line computational proof: by decide. Lean reduces both sides of the integer equality (the fold that defines the numerator, and eight times the matched table clause) to concrete Int values and checks they coincide. No lemmas are invoked beyond the definitions of the numerator fold and the explicit table.

The parent theorem m2Num_eq_eight_explicitZ assembles every index tuple into the universal statement $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$. That assembly runs nested fin_cases over the six Fin 4 arguments and discharges each leaf by a chunk theorem of this form.

In the Recognition gravity stack, the identity certifies that the midpoint-evaluated M2–TT coupling on the 4D lattice collapses to a sparse, explicitly tabulated integer kernel. That kernel is the algebraic substrate for later continuum and phenomenological limits in the discrete gravity analysis; without the case-by-case match, the closed form cannot be trusted inside larger proofs.