e_022101
plain-language theorem explainer
For the six-index tuple (0,2,2,1,0,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it as one cell of the 4^6 case split that proves the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on two closed integer expressions.
Claim. For indices $a=0$, $b=2$, $c=2$, $d=1$, $i=0$, $j=1$ in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
This module is chunk 2 of a machine-checked verification that the 4D Regge midpoint $M_2$ numerator equals eight times an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$. The local slogan is "$m_2^{\mathrm{num}} = 8\cdot Z$, chunk 2 (256 kernel decides)."
Upstream, $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 target $Z$ is an explicit piecewise integer function on the same six $\mathrm{Fin},4$ arguments (sample clauses include $Z(0,0,1,1,2,2)=4$ and $Z(0,0,1,2,1,2)=-2$).
The present declaration fixes one concrete cell of that six-fold table: indices $(0,2,2,1,0,1)$.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six indices are substituted into the fold definition of the numerator and the pattern-matching definition of the explicit kernel; the kernel then discharges equality of those integers. No lemmas beyond the two upstream definitions are invoked.
why it matters
The parent theorem is m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j:\mathrm{Fin},4,; m_2^{\mathrm{num}}=8Z$. Its proof is a pure fin_cases tree on all six indices; each leaf is one of these chunk theorems (siblings e_020000, e_020001, …). This cell closes the branch for $(0,2,2,1,0,1)$.
In the broader Gravity analysis stack, the identity certifies that the midpoint $M_2$ TT kernel in 4D Regge calculus matches its closed-form integer table, so later curvature and continuum-limit arguments can quote the compact $8Z$ form instead of the fold. It is bookkeeping inside the certified kernel, not a new physical law, but without the full case cover the assembly theorem does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.