e_312233
plain-language theorem explainer
For the multi-index (3,1,2,2,3,3) on Fin 4, the folded coupling numerator m2Num equals eight times the explicit integer table explicitZ. Gravity analysts cite it as one atomic case of the 4D Regge midpoint M2–TT kernel identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3,\,b{=}1,\,c{=}2,\,d{=}2,\,i{=}3,\,j{=}3$ in $\mathrm{Fin}\,4$, the summed coupling numerator equals eight times the explicit closed-form integer: $\mathrm{num}(3,1,2,2,3,3)=8\,Z(3,1,2,2,3,3)$.
background
This module is one chunk of the 4D Regge exact-midpoint M2–TT identity: the claim that the folded numerator built from the coupling list equals eight times a sparse explicit integer table, case by case on $(\mathrm{Fin},4)^6$.
The numerator is defined by folding couplingZList and summing a local contribution at each multi-index $(a,b,c,d,i,j)$. The comparison target explicitZ is a pattern-matched integer table on the same six Fin-4 arguments (typical nonzero entries are $\pm 2,,4$).
Chunk 13 packages 256 such kernel decides. Upstream, only the two defs matter: the fold that builds the numerator and the explicit table it is checked against.
proof idea
One-line computational proof: by decide. Both sides reduce to concrete Int values for the fixed sextuple $(3,1,2,2,3,3)$, so the kernel equality checker discharges the goal with no lemmas or rewriting.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states the identity for every $(a,b,c,d,i,j):(\mathrm{Fin},4)^6$ and proves it by exhaustive fin_cases. Each chunk theorem such as this one is an atomic cell in that $4^6$ grid.
In the gravity analysis stack this closes the numerator side of the Regge midpoint M2–TT kernel certificate: once every cell matches $8\cdot Z$, the closed form may replace the fold in downstream curvature or deficit identities. It is pure discrete bookkeeping, not a continuum GR claim, and sits inside the RS gravity analysis layer rather than the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.