e_011101
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at Fin-4 indices (0,1,1,1,0,1) equals eight times the explicit integer table at that same sextuple. Gravity analysts cite it as one cell of the 256-way kernel that underwrites the global m2Num = 8·explicitZ statement. The proof is a single kernel decide on concrete integers.
Claim. For the index sextuple $(a,b,c,d,i,j)=(0,1,1,1,0,1)$ with each coordinate in $\mathbb{F}_4$, the folded coupling numerator equals eight times the explicit integer value: $m_2^{\mathrm{num}}(0,1,1,1,0,1)=8\,Z_{\mathrm{expl}}(0,1,1,1,0,1)$.
background
This module is chunk 1 of a 256-cell kernel certifying the exact midpoint identity $m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ in the 4D Regge analysis. Indices run over $\mathrm{Fin},4$, i.e. residue classes ${0,1,2,3}$.
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 $\mathrm{contrib}(t;a,b,c,d,i,j)$. The comparison target $Z_{\mathrm{expl}}$ is an explicit integer-valued table on six $\mathrm{Fin},4$ arguments (sample clauses include $(0,0,1,1,2,2)\mapsto 4$ and $(0,0,1,2,1,2)\mapsto -2$).
The local claim is only the single sextuple $(0,1,1,1,0,1)$; sibling theorems cover the other cells of the same chunk.
proof idea
One-line kernel proof: by decide. Both sides reduce to concrete integers once the fold for $m_2^{\mathrm{num}}$ and the pattern match for $Z_{\mathrm{expl}}$ are evaluated at the fixed indices $(0,1,1,1,0,1)$, so the equality is a closed arithmetic fact discharged by Lean's decision procedure. No lemmas are invoked beyond the two defining defs.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8,Z_{\mathrm{expl}}$ by exhaustive fin_cases on all six arguments. Each cell such as this one is a leaf of that case tree; without the pointwise decides the global identity does not close.
In the broader gravity stack this identity is bookkeeping for the exact midpoint M2TT 4D kernel: it replaces a folded coupling sum by a sparse explicit integer table, which is the form needed for later closed-form Regge curvature and mass-ladder comparisons. It is infrastructure, not a forcing-chain landmark (T5–T8), but it is required scaffolding for the 4D gravity numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.