e_011010
plain-language theorem explainer
At multi-index (0,1,1,0,1,0) the folded Regge coupling numerator equals eight times the explicit integer table entry. Gravity analysts cite this as one cell of the 256-point kernel that certifies the closed-form identity. The proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,1,0,1,0)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: sum the local contributions of each term at a six-index in $(\mathrm{Fin},4)^6$. The companion table $Z$ is an explicit integer pattern on those same indices (nonzero only on a sparse set of matchings such as $(0,0,1,1,2,2)\mapsto 4$).
This module is chunk 1 of the kernel certification that $m_2^{\mathrm{num}}=8Z$ pointwise. The local setting is pure finite enumeration: every index is a concrete Fin 4, so each cell is a closed integer identity.
Upstream, $m_2^{\mathrm{num}}$ is the fold over couplingZList, and $Z$ is the case-split table used as the closed form.
proof idea
One-line kernel proof: decide evaluates both sides at the fixed six-tuple $(0,1,1,0,1,0)$ and checks integer equality. No lemmas are invoked beyond the definitions of the fold and the table.
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$ by exhausting all Fin 4 cases and dispatching each cell to a chunk theorem of this form. That global identity is the algebraic core of the Regge exact midpoint $M_2$ TT certificate in 4D gravity analysis inside the monolith. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the discrete curvature/mass-squared side of the gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.