e_000211
plain-language theorem explainer
Single kernel point check: the Regge midpoint numerator at multi-index (0,0,0,2,1,1) equals eight times the explicit closed-form kernel value at that same index. Gravity analysts cite it only as one cell of the 256-way case split that builds the global identity. The proof is a pure `decide` on concrete integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(0,0,0,2,1,1)$ with each coordinate in $\mathbb{F}_4$, the integer numerator $m_2^{\mathrm{num}}(0,0,0,2,1,1)$ equals $8\,Z(0,0,0,2,1,1)$, where $Z$ is the explicit six-index kernel table and $m_2^{\mathrm{num}}$ is the fold of coupling contributions over that table.
background
This module is chunk 0 of a 256-cell kernel certification that the 4D Regge exact-midpoint $M_2$ numerator agrees with eight times an explicit integer table. Indices run over $\mathrm{Fin},4$, i.e. four discrete directions in the simplicial complex.
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 each contribution term at those six indices. The comparison object $Z(a,b,c,d,i,j)$ is a pattern-matched integer table (values such as $4$, $-2$, and so on) that packages the closed-form kernel.
The local claim is only the equality at one concrete six-tuple. Sibling theorems cover the other tuples in the same chunk; the assembly theorem quantifies over all of $\mathrm{Fin},4^6$.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values (the left via the fold definition of the numerator, the right via the pattern match on the explicit table, then multiplication by 8), and Lean’s decision procedure discharges the integer equality. No lemmas are invoked beyond the two definitions.
why it matters
Feeds the assembly 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, each leaf a chunk theorem of this form. That global identity is the algebraic core of the 4D Regge exact-midpoint $M_2$ TT-kernel certification in the Gravity analysis stack. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete-kernel bookkeeping needed before continuum or phenomenological gravity claims can cite an exact midpoint formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.