e_111100
plain-language theorem explainer
For the six-index pattern (1,1,1,1,0,0) on Fin 4, the folded midpoint numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one cell of the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=d=1$ and $i=j=0$ in $\mathrm{Fin}\,4$, the midpoint numerator $m_2^{\mathrm{num}}(1,1,1,1,0,0)$ equals $8\,Z(1,1,1,1,0,0)$, where $Z$ is the explicit integer kernel table.
background
This module is chunk 5 of a 256-cell decide grid proving that the folded midpoint numerator equals eight times an explicit integer kernel on every 4D index sextuple. The ambient setting is the exact midpoint identity for the Regge-style M2 tensor in four dimensions.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing a local contribution at each term. The comparison target $Z(a,b,c,d,i,j)$ is a sparse pattern-matched integer table on $\mathrm{Fin},4^6$ (nonzero only on a handful of index geometries such as paired diagonals and crossed pairs).
The full statement is assembled downstream by exhaustive fin_cases over all six indices; each chunk theorem discharges one concrete cell so the assembler stays lightweight.
proof idea
One-line decide proof. Both sides reduce to concrete Int values for the fixed arguments $(1,1,1,1,0,0)$: the left via the fold definition of the numerator, the right via the pattern match on the explicit kernel (or the default zero branch). Lean’s kernel decision procedure checks integer equality.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which asserts the identity for every sextuple in $\mathrm{Fin},4$ by casing through all $4^6$ cells and invoking the matching chunk lemma at each leaf. That global equality is the algebraic certificate that the midpoint M2 numerator is exactly eight copies of the closed-form kernel, a step in the exact 4D Regge midpoint analysis used on the gravity side of the monolith.
It does not itself touch the forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete tensor bookkeeping supporting the continuum/Regge gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.