e_320333
plain-language theorem explainer
At multi-index (3,2,0,3,3,3) the folded Regge coupling numerator equals eight times the explicit integer table value. Gravity analysts cite it as one atomic kernel cell in the 4D midpoint M2–TT identity. The proof is a pure `decide` on concrete integers.
Claim. For indices $a{=}3,b{=}2,c{=}0,d{=}3,i{=}3,j{=}3$ in $\mathbb{F}_4$, the folded coupling numerator $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit table entry $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis the numerator $m_2^{\mathrm{num}}$ is defined by folding a fixed coupling list: each term contributes an integer contrib at six $\mathrm{Fin},4$ indices, and the fold starts from zero. The companion table explicitZ is a sparse pattern-matched integer function on the same six indices (nonzero only on a short list of ordered sextuples, with values such as $\pm 2,\pm 4$).
The local module is chunk 14 of a 256-cell kernel certification whose sole job is to check $m_2^{\mathrm{num}}=8\cdot Z$ pointwise. The ambient claim is the exact midpoint M2–TT identity in four dimensions; this file only discharges one concrete index cell.
proof idea
One-line computational proof: decide evaluates both sides at the literal indices $(3,2,0,3,3,3)$ and confirms integer equality. No lemmas are invoked beyond the definitions of m2Num (the fold) and explicitZ (the table).
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every sextuple in $(\mathrm{Fin},4)^6$ by exhaustive fin_cases. That global equality is the algebraic core of the Regge exact-midpoint M2–TT certification in 4D gravity. The chunk exists only to keep the kernel decidable in small pieces; it does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law, but it is load-bearing for the discrete curvature side of the RS gravity stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.