e_033122
plain-language theorem explainer
Case check that the folded coupling numerator equals eight times the explicit integer table at multi-index (0,3,3,1,2,2). Gravity analysts cite it only as one atom of the 4^6 case split that proves the global m2Num = 8·explicitZ identity. The proof is a single kernel decide on two concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,3,3,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 table value $Z(a,b,c,d,i,j)$.
background
This module is chunk 3 of a brute-force certification that, on every 6-tuple of $\mathrm{Fin},4$ indices, the numerator $m_2^{\mathrm{num}}$ of a Regge midpoint mass-squared coupling equals eight times a closed-form integer table $Z$. The setting is 4D discrete gravity analysis (exact midpoint M2TT identity).
Upstream, $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: start at $0$ and add each contribution $\mathrm{contrib}(t;a,b,c,d,i,j)$. The table $Z$ is an explicit pattern-match on the six indices, returning small integers such as $4$, $-2$, and so on. Both sides are pure $\mathrm{Int}$-valued functions of six finite indices, so each concrete tuple is decidable.
proof idea
One-line kernel proof: decide. Both sides reduce to concrete integers (the left by evaluating the fold of contributions at the fixed indices $0,3,3,1,2,2$; the right by looking up $8\cdot Z(0,3,3,1,2,2)$), and the kernel checks equality.
why it matters
Parent theorem is m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,; m_2^{\mathrm{num}}=8,Z$ and is proved by exhaustive fin_cases on all six $\mathrm{Fin},4$ arguments. Each leaf of that case tree is one of these chunk lemmas (siblings e_030000, …). The factor-of-eight identity is the algebraic core of the Regge exact-midpoint M2TT certification in 4D: once numerator and table match everywhere, the continuum-limit coupling analysis can quote a single closed form instead of a fold. No Recognition forcing-chain landmark (T5–T8, RCL, $\varphi$) is invoked here; this is pure finite combinatorial bookkeeping inside the gravity analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.