e_220231
plain-language theorem explainer
For the single multi-index (2,2,0,2,3,1) in (Fin 4)^6, the Regge midpoint M2 numerator equals eight times the explicit Z coupling value. Gravity analysts cite it as one atomic case in the 4D TT-identity kernel. The proof is a pure kernel decision (`decide`) with no algebraic rewriting.
Claim. For indices $a{=}2,b{=}2,c{=}0,d{=}2,i{=}3,j{=}1$ in $\mathbb{F}_4$, the midpoint $M_2$ numerator equals eight times the explicit coupling: $m_2^{\mathrm{num}}(2,2,0,2,3,1)=8\,Z(2,2,0,2,3,1)$.
background
This module sits inside the 4D Regge exact-midpoint analysis for the TT sector. The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at a sextuple of $\mathrm{Fin},4$ indices, and the fold starts from 0. The comparison target explicitZ is a closed-form integer table on the same six indices (pattern-matched constants such as $4$, $-2$, and so on).
The local claim of the file is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ on the full $4^6$ kernel, discharged in chunks of decide lemmas. Chunk 10 supplies one block of those atomic equalities; the present declaration is the case with indices $(2,2,0,2,3,1)$.
proof idea
One-line kernel proof: by decide. Both sides are closed integer expressions once the six concrete Fin 4 arguments are substituted into the fold definition of the numerator and the pattern table for explicit $Z$, so the equality is a decidable computation on Int with no further lemmas.
why it matters
The parent assembly theorem m2Num_eq_eight_explicitZ states the universal identity $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and proves it by exhaustive fin_cases on all six indices. Each atomic goal lands on a chunk lemma of this form; the present case closes the $(2,2,0,2,3,1)$ cell.
In the broader gravity stack this identity is the algebraic certificate that the midpoint $M_2$ TT kernel matches the explicit eightfold coupling table, a necessary numerical step before continuum or continuum-limit comparisons in the Regge sector. It does not itself invoke the RS forcing chain (T5–T8) or the J-cost; it is pure discrete-kernel bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.