e_112232
plain-language theorem explainer
For the multi-index (1,1,2,2,3,2) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel entry. Gravity analysts certifying the 4D Regge midpoint M2TT identity cite it as one of 256 exhaustive index cases. Proof is a single kernel decide on closed integer arithmetic.
Claim. For indices $a=1$, $b=1$, $c=2$, $d=2$, $i=3$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated explicit integer: $N(1,1,2,2,3,2)=8\,Z(1,1,2,2,3,2)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on six Fin-4 indices are compared pointwise. The numerator $N(a,b,c,d,i,j)$ is defined by folding a contribution function over a fixed coupling list, starting from zero. The companion map $Z$ is an explicit sparse table of small integers (entries such as $4$ and $-2$ on selected multi-indices).
The local module is chunk 5 of a 256-case kernel bash whose sole job is to check $N=8Z$ at every multi-index. Upstream, both maps live in the kernel-certificate module that supplies the concrete definitions used here.
proof idea
One-line wrapper: by decide. Both sides are closed integer terms once the six Fin-4 literals are substituted. The kernel evaluates the fold that defines the numerator and the pattern match that defines the explicit table, then confirms the two integers are equal. No lemmas are invoked beyond reduction of the two defining defs.
why it matters
This case is consumed by the universal assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ and discharges the quantifiers by fin_cases on all six indices. That pointwise identity is a certificate step inside the 4D Regge exact-midpoint M2TT analysis: it shows the folded coupling numerator is exactly eight times the sparse explicit kernel, so the two presentations of the discrete curvature coupling may be swapped freely in later gravity identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.