e_312112
plain-language theorem explainer
For the multi-index (3,1,2,1,1,2) on Fin 4, the folded coupling numerator equals eight times the tabulated explicit kernel value. Gravity analysts cite it when assembling the full 4D Regge midpoint M2TT identity over all sextuples. The proof is a single kernel decide on that concrete integer equality.
Claim. For indices $a=3$, $b=1$, $c=2$, $d=1$, $i=1$, $j=2$ in $\{0,1,2,3\}$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit kernel table entry $Z(a,b,c,d,i,j)$.
background
This module is one chunk of a 256-case kernel certification that the 4D Regge exact-midpoint M2TT numerator matches eight times a closed-form table. The numerator is defined by folding a fixed coupling list: each term contributes an integer depending on the six Fin-4 indices, and the fold starts at 0. The explicit table is a pattern-matched integer function on the same six indices (typical values $\pm 2,,4$, and sparse support).
The local setting is pure integer arithmetic on a finite index set: no continuum limit, no floating point. Upstream, the numerator and the table are pure defs in the kernel-cert module; this chunk only checks one concrete sextuple against the claimed factor of eight.
proof idea
One-line computational proof: decide evaluates both sides at the fixed indices $(3,1,2,1,1,2)$ and checks integer equality. No lemmas are invoked beyond the definitions of the folded numerator and the explicit table; the kernel closes the goal by reduction.
why it matters
Parent theorem is the full universal statement that the numerator equals eight times the explicit table for every Fin-4 sextuple. That assembler runs nested fin-cases and lands on chunk theorems such as this one for each concrete index pattern. Closing the factor-of-eight identity is bookkeeping inside the 4D Regge midpoint M2TT analysis: it certifies that the expanded coupling sum collapses to the sparse closed form used downstream in the gravity stack. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is infrastructure for the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.