e_232111
plain-language theorem explainer
For the multi-index (2,3,2,1,1,1) on Fin 4, the folded Regge midpoint coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one of 256 kernel certificates for the 4D midpoint m2 identity. The proof is a single decide on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(2,3,2,1,1,1)$ in $(\mathbb{F}_4)^6$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-case kernel certifying $m_2^{\mathrm{num}}=8\cdot Z$ for the exact midpoint Regge identity in 4D. Indices run over $\mathrm{Fin},4$, so the full statement is a finite table identity.
The numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: start at $0$ and add a contribution term for each coupling triple at the six indices. The comparison target $Z$ is an explicit integer-valued pattern match on those same six indices (sample clauses return $4$, $-2$, and so on).
The local goal is only the single tuple $(2,3,2,1,1,1)$. Sibling lemmas cover the other tuples in the same chunk; the assemble theorem glues all cases.
proof idea
One-line computational proof: decide. Both sides are closed integer expressions once the six $\mathrm{Fin},4$ arguments are concrete literals, so the kernel reduces the equality without further lemmas. No algebraic rewriting is needed beyond evaluation of the fold and the $Z$ match.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):\mathrm{Fin},4$ by exhaustive fin_cases. That global equality is the certified numerator form of the 4D Regge exact-midpoint $m_2$ identity used in the gravity analysis stack.
In the Recognition framework this sits in the discrete gravity / Regge sector: a finite, machine-checked table identity rather than a continuum variational argument. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is infrastructure for the midpoint curvature bookkeeping that those continuum claims eventually rely on when gravity is reduced to combinatorial data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.