e_212232
plain-language theorem explainer
For the discrete index sextuple (2,1,2,2,3,2) on Fin 4, the folded coupling numerator m2Num equals eight times the tabulated explicit integer Z. Gravity analysts cite it as one atomic case in the 4D Regge midpoint M2/TT identity. The proof is a single kernel decide on concrete integers.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Write $N$ for the coupling numerator obtained by folding the fixed contribution list at those indices, and $Z$ for the tabulated explicit integer at the same indices. Then $N(2,1,2,2,3,2)=8\,Z(2,1,2,2,3,2)$.
background
This module is chunk 9 of a finite case-split proving that the 4D Regge-exact midpoint coupling numerator equals eight times an explicit integer table. Indices run over $\mathrm{Fin},4$ (values $0..3$), six of them at a time, matching the discrete legs of the midpoint M2/TT kernel.
Upstream, m2Num is defined by folding a fixed list couplingZList and summing a local contribution at $(a,b,c,d,i,j)$. The companion explicitZ is a total function $\mathrm{Fin},4^6\to\mathbb{Z}$ given by a finite pattern of integer clauses (e.g. $(0,0,1,1,2,2)\mapsto 4$, mixed pairs $\mapsto -2$, and so on). The claim is the pointwise identity $N=8Z$ at one concrete sextuple.
The local setting is pure integer arithmetic on a closed finite domain: no continuum limit, no floating point, only kernel-checkable equalities.
proof idea
One-line computational proof: decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are literals, so the kernel closes the equality without lemmas or rewriting. No induction and no appeal to the global fold structure beyond evaluation of the two definitions.
why it matters
The parent theorem m2Num_eq_eight_explicitZ asserts $\forall a,b,c,d,i,j,; N=8Z$ and discharges the universal quantifier by exhaustive fin_cases on all six indices. Each atomic goal is one of these chunk theorems; this declaration supplies the case $(2,1,2,2,3,2)$.
In the Recognition gravity stack the identity certifies that the discrete midpoint M2/TT numerator is exactly eight copies of a sparse explicit table, which is the algebraic backbone for the Regge-exact 4D kernel certificates imported here. It is bookkeeping rather than a new physical law, but without the full case cover the assembly theorem cannot close.
No open scaffold remains on this sextuple: the equality is decided.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.