e_122302
plain-language theorem explainer
For the six-index tuple (1,2,2,3,0,2) in (Fin 4)^6, the Regge midpoint mass-squared numerator equals eight times the explicit integer Z-coupling. Gravity analysts cite it as one kernel cell of the 4D midpoint M2–TT identity. The proof is a single kernel decide on concrete integers.
Claim. At multi-index $(a,b,c,d,i,j)=(1,2,2,3,0,2)$ with each coordinate in $\{0,1,2,3\}$, the folded mass-squared numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit coupling value $Z(a,b,c,d,i,j)$.
background
This module is chunk 6 of a 256-cell kernel certification that the 4D Regge midpoint mass-squared numerator agrees with eight times a closed-form integer table. The ambient setting is discrete gravity analysis: edge and face couplings on a 4-simplex lattice with midpoint evaluation of the TT sector.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add each local contribution at the six Fin-4 indices. The comparison target $\mathrm{explicit}Z$ is a pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on). The claim is the pointwise identity at one concrete multi-index.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(1,2,2,3,0,2)$. The left side reduces by unfolding the fold over the coupling list; the right side reduces by unfolding the pattern match for $\mathrm{explicit}Z$; integer equality is then discharged by the kernel.
why it matters
The cell is consumed by the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every six-tuple in $(\mathrm{Fin},4)^6$ by exhaustive case split. That global equality is the algebraic backbone of the Regge-exact midpoint M2–TT identity in 4D used in the gravity analysis stack. It does not itself invoke the RS forcing chain (T5–T8) or the Recognition Composition Law; it is pure discrete-geometry bookkeeping that later continuum or continuum-limit arguments can quote without rechecking the table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.