e_213100

This module is chunk 9 of a 256-cell kernel certification that the Regge midpoint numerator $m_2^{\mathrm{num}}$ factors as eight times an explicit integer table $Z$ on six $\mathrm{Fin},4$ indices. The setting is 4D discrete gravity analysis: couplings are summed from a fixed list, and the identity is checked pointwise.

Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding couplingZList and accumulating each contribution at those indices. The companion table $Z$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on for distinguished index patterns).

The full statement is the universal quantification over all $4^6$ tuples; each chunk theorem pins one concrete cell so the assembler can discharge the forall by exhaustive fin_cases.

One-line proof by decide. Both sides are closed integer expressions once the six Fin-4 indices are substituted: the left side evaluates the fold that defines the numerator, the right side multiplies the pattern-matched kernel entry by eight. Lean’s kernel decision procedure compares the two concrete integers and closes the goal.

Feeds the assembler theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and proves it by nested fin_cases over all six indices, invoking one cell theorem per branch. Without the chunk equalities the universal identity does not typecheck as proved.

In the Recognition gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D Regge calculus: it certifies that the folded coupling numerator is exactly eight copies of the closed-form $Z$ table, so later curvature and continuum-limit arguments can quote a single sparse integer kernel rather than a fold. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete-kernel arithmetic supporting the gravity analysis layer.