e_123333
plain-language theorem explainer
At multi-index (1,2,3,3,3,3) the folded coupling numerator equals eight times the explicit integer Z-table entry. Gravity analysts cite it as one atomic kernel check inside the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(1,2,3,3,3,3)$ 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
In the 4D Regge exact-midpoint analysis the numerator mass-squared coupling is defined by folding a fixed contribution list: $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ sums contrib over couplingZList. The companion table $Z$ is an explicit sparse map $(\mathbb{F}_4)^6\to\mathbb{Z}$ with a handful of nonzero integer entries (e.g. $\pm 2,4$).
The local module is chunk 6 of a 256-way partition of the finite index space. Each chunk discharges a block of concrete equalities $m_2^{\mathrm{num}}=8Z$ by kernel decision, so the later assembly theorem can reassemble the universal statement by fin_cases on all six coordinates.
proof idea
One-line tactic proof: decide. Both sides reduce to concrete Int values (the fold of m2Num at the fixed six-tuple versus eight times the matching explicitZ clause), and the kernel checks integer equality. No lemmas are invoked beyond the definitions of m2Num and explicitZ.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j:\mathbb{F}_4,; m_2^{\mathrm{num}}=8Z$ by exhaustive fin_cases and the chunk equalities. That identity is the certified numerator half of the Regge exact-midpoint M2TT relation in four dimensions, inside the Gravity analysis layer of the monolith. It is pure finite-check scaffolding for the continuum claim, not itself a continuum or curvature theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.