e_010221
plain-language theorem explainer
Pointwise check that the Regge midpoint numerator m2Num at indices (0,1,0,2,2,1) equals eight times the explicit integer table explicitZ at the same point. Gravity analysts cite it as one cell of the 256-case kernel that builds the global m2Num = 8·explicitZ identity. The proof is a single decide on concrete Fin-4 integers.
Claim. At the index tuple $(a,b,c,d,i,j)=(0,1,0,2,2,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table value: $m_2^{\mathrm{num}}(0,1,0,2,2,1)=8\,Z_{\mathrm{expl}}(0,1,0,2,2,1)$.
background
This module is chunk 1 of the 256 kernel decides that establish $m_2^{\mathrm{num}}=8\cdot Z_{\mathrm{expl}}$ for the exact midpoint M2TT identity in 4D Regge gravity analysis.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is the fold of contrib over couplingZList, returning an integer for each sextuple of $\mathrm{Fin},4$ indices. The companion table $Z_{\mathrm{expl}}$ is a closed-form pattern-matched integer function on the same domain (sample clauses include values $4$, $-2$, and so on).
The local goal is not conceptual: it is exhaustive verification that the folded sum matches eight times the table at every concrete point, so a later assembler can quote a universal equality.
proof idea
One-line computational proof: decide. Both sides are closed integer terms once the six $\mathrm{Fin},4$ arguments are literals, so the kernel evaluates $m_2^{\mathrm{num}}(0,1,0,2,2,1)$ and $8\cdot Z_{\mathrm{expl}}(0,1,0,2,2,1)$ and checks equality by native decision.
why it matters
Feeds the assembler 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}}$ and discharges the universal claim by nested fin_cases over all six indices. Each concrete cell such as this one is a leaf of that case split.
In the gravity stack this identity is bookkeeping for the exact midpoint M2TT kernel in 4D: it certifies that the summed coupling numerator is a uniform multiple of the explicit integer table, so later curvature or deficit identities can substitute the closed form. It does not itself touch the T0–T8 forcing chain or the Recognition Composition Law; it is infrastructure inside the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.