e_221122
plain-language theorem explainer
At multi-index (2,2,1,1,2,2) the folded Regge coupling numerator equals eight times the explicit integer kernel value. Gravity analysts assembling the 4D midpoint M2 TT identity cite this as one concrete cell of chunk 10. The proof is a single kernel decide on fully evaluated integers.
Claim. For indices $(a,b,c,d,i,j)=(2,2,1,1,2,2)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit kernel integer $Z(a,b,c,d,i,j)$.
background
The ambient module is a chunked verification that the 4D Regge midpoint M2 TT numerator agrees with eight times an explicit integer kernel on every multi-index in $(\mathrm{Fin},4)^6$. Module doc: "m2Num = 8·explicitZ, chunk 10 (256 kernel decides)."
The numerator $m_2^{\mathrm{num}}$ is the fold of a fixed coupling list: start at 0 and add each term's contribution at the six indices. The explicit kernel $Z$ is a pattern-matched integer table on those same six $\mathrm{Fin},4$ arguments (sample clauses give values such as $4$, $-2$, and so on).
Chunk 10 is one block of the $4^6$ case grid. Sibling lemmas cover neighboring index tuples; together they feed the universal assembly theorem.
proof idea
One-line wrapper: by decide. Both sides reduce to concrete Int values once the six numerals are substituted. The left side runs the fold that defines the numerator; the right side multiplies the matched kernel clause by 8. No lemmas are invoked beyond the definitions of the numerator and the explicit kernel; the kernel closes the integer equality.
why it matters
Parent theorem is the universal identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8Z$ and discharges the quantifiers by exhaustive fin_cases on each $\mathrm{Fin},4$ coordinate. This lemma is the cell for indices $(2,2,1,1,2,2)$ inside that case tree (chunk 10).
In the Recognition gravity stack the identity is bookkeeping for the exact midpoint M2 TT sector of 4D Regge calculus: once every cell matches, the assembled numerator may be replaced by the closed-form kernel. It does not itself touch the forcing chain (T0–T8), $\phi$-ladder masses, or the $\alpha$ band; it is pure discrete-tensor arithmetic supporting the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.