e_233131
plain-language theorem explainer
One of 256 concrete kernel identities: the midpoint Regge mass-squared numerator at multi-index (2,3,3,1,3,1) equals eight times the explicit integer Z-coupling at that same index. The global Fin-4 assembly theorem cites every such chunk. Proof is a single kernel decide on fixed integers.
Claim. For the multi-index $(a,b,c,d,i,j)=(2,3,3,1,3,1)$ with each entry in $\{0,1,2,3\}$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel $Z(a,b,c,d,i,j)$.
background
This module is chunk 11 of a 256-way case split proving $m_2^{\mathrm{num}}=8\cdot Z$ on all of $(\mathrm{Fin},4)^6$. The setting is the exact midpoint identity for a 4D Regge-type mass-squared numerator in the gravity analysis stack.
The numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each term's contribution at the six indices. The comparison object $Z$ is an explicit integer-valued kernel on the same six $\mathrm{Fin},4$ arguments, given by a finite pattern of constants (e.g. $4$, $-2$, and symmetric permutations).
Both definitions live in the kernel-certificate module imported here. The present declaration fixes one concrete six-tuple and asserts numerical equality after the factor of eight.
proof idea
One-line proof by decide. Both sides reduce to concrete integers: the left-hand side evaluates the fold of couplingZList contributions at indices $(2,3,3,1,3,1)$; the right-hand side is $8$ times the matching clause of the explicit $Z$ table. Lean’s kernel decision procedure discharges the integer equality with no further lemmas.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8\cdot Z$ by exhaustive fin_cases on all six indices. Each chunk such as this one supplies one (or a block of) decided equalities so the global identity is a pure case cover rather than a symbolic simplification of the fold.
In the Recognition gravity analysis, that identity is the certified algebraic core of the exact midpoint $M_2$ TT relation in 4D: once numerator and explicit kernel match up to the universal factor eight, downstream curvature and mass-ladder comparisons can quote a single closed form instead of the folded sum. No forcing-chain landmark (T5–T8) is touched directly; this is infrastructure inside the Regge/midpoint gravity layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.