e_010110
plain-language theorem explainer
For the six-index slot (0,1,0,1,1,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the exact midpoint M2 TT identity cite this as one of the 256 kernel cells. The proof is a pure kernel decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,1,1,0)$ in $\mathrm{Fin}\,4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
This module is chunk 1 of a 256-cell kernel certification that the Regge midpoint numerator equals eight times a closed-form table. Indices run over $\mathrm{Fin},4$, matching a 4D simplex/edge labeling in the Regge calculus setup.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution contrib t a b c d i j. The comparison target explicitZ is a sparse integer table on six $\mathrm{Fin},4$ arguments (nonzero only on a short list of index patterns such as $(0,0,1,1,2,2)\mapsto 4$ and several $-2$ off-diagonal patterns).
The local claim is the single cell $(0,1,0,1,1,0)$ of the identity $m_2^{\mathrm{num}}=8,Z$. Sibling theorems cover the other cells in the same chunk.
proof idea
One-line decide proof. Both sides reduce to concrete Int values: the left by evaluating the fold of couplingZList at the fixed indices, the right by multiplying the table lookup explicitZ 0 1 0 1 1 0 by 8. Lean’s kernel decision procedure checks integer equality; no lemmas are invoked.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and discharges the universal quantifier by fin_cases on all six indices, routing each cell to a chunk theorem of this form.
In the gravity analysis stack this identity is the exact algebraic midpoint step for the 4D M2 TT kernel: once every cell matches, the folded coupling numerator may be replaced by the closed table explicitZ under the factor 8. That replacement is bookkeeping for the Regge-exact midpoint identities used downstream in the Recognition gravity development, not a new dynamical law. It does not itself invoke the T0–T8 forcing chain, RCL, or $\varphi$-ladder mass formula; it is pure finite combinatorial certification inside the 4D index kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.