e_012121
plain-language theorem explainer
For the six-index tuple (0,1,2,1,2,1) on Fin 4, the folded Regge coupling numerator equals eight times the explicit integer Z table. Gravity analysts cite it when discharging one kernel cell of the 4D midpoint M2TT identity. The proof is a single computational decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,2,1,2,1)$ with each index 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 table entry $Z(a,b,c,d,i,j)$.
background
This module is one cell of the 4D Regge midpoint analysis: it certifies the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on a fixed multi-index, as part of a 256-way kernel split (chunk 1).
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each contribution term at the six Fin-4 indices. The comparison table $Z$ is an explicit pattern-matched integer function on the same six indices (sample values include $4$, $-2$, and so on for the listed patterns).
The local goal is purely algebraic bookkeeping: evaluate both sides at one concrete tuple and record equality, so a later assembler can quantify over all $4^6$ index combinations.
proof idea
One-line computational proof: decide. Both sides reduce to concrete integers once the six Fin-4 arguments are literals, so the kernel closes the equality by evaluation. No lemmas beyond the definitions of the folded numerator and the explicit $Z$ table are required.
why it matters
Feeds the assembler theorem that states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$, proved there by exhaustive fin_cases on the six indices. Each chunk theorem such as this one is a named kernel cell in that case split.
In the broader gravity stack this is infrastructure for the exact midpoint M2TT identity in 4D Regge calculus: matching the folded coupling numerator to a closed integer table clears a bookkeeping obligation before continuum or continuum-limit arguments. It does not itself invoke the RS forcing chain (T5–T8), phi, or the eight-tick octave; it is a finite combinatorial certificate inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.