e_333121
plain-language theorem explainer
At multi-index (3,3,3,1,2,1) on Fin 4, the folded numerator coupling equals eight times the explicit Z-kernel entry. Gravity analysts cite it when assembling the full pointwise identity m2Num = 8·explicitZ over the 4D midpoint Regge kernel. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=b=c=3$, $d=1$, $i=2$, $j=1$ in $\mathrm{Fin}\,4$, the folded numerator coupling $m_2^{\mathrm{num}}(a,b,c,d,i,j)$ equals $8$ times the explicit integer kernel value $Z(a,b,c,d,i,j)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator coupling $m_2^{\mathrm{num}}$ is defined by folding a contribution function over a fixed coupling list: start at 0 and accumulate each term's contrib at the given multi-index. The explicit kernel $Z$ is a piecewise integer table on the same six indices (sample values include $4$, $-2$, and other small constants on listed patterns).
This module is chunk 15 of a 256-way partition of the Fin-4^6 domain. The local claim is the pointwise identity $m_2^{\mathrm{num}}=8\cdot Z$ at one concrete tuple. The parent assembly theorem states the same equality for every six-tuple and discharges it by exhaustive fin_cases, each leaf matching one chunk decide such as this one.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin-4 indices (3,3,3,1,2,1). The left side runs the fold that defines $m_2^{\mathrm{num}}$; the right side looks up $Z$ and multiplies by 8. Both reduce to the same integer, so the equality is closed by the kernel decision procedure. No lemmas beyond the two defining defs are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which asserts $\forall a,b,c,d,i,j,, m_2^{\mathrm{num}}=8\cdot Z$ and proves it by six nested fin_cases over Fin 4. Each leaf is one of the 256 chunk decides; this declaration is the leaf for (3,3,3,1,2,1).
In the broader Gravity analysis, that universal identity is the certified numerator half of the exact midpoint M2 TT identity in 4D Regge calculus. It sits downstream of the kernel certificate module and upstream of any continuum or continuum-limit reading of the discrete curvature coupling. It does not itself touch the forcing chain (T0–T8), RCL, or the phi-ladder mass formula; those enter only if later gravity layers import this certified discrete identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.