e_010111
plain-language theorem explainer
Pointwise identity: the folded Regge coupling numerator at index sextuple (0,1,0,1,1,1) equals eight times the explicit integer table at that point. One of 256 kernel decides in chunk 1 of the m2Num = 8·explicitZ certification. The assembly theorem cites it when exhausting all Fin-4 sextuples. Proof is a single kernel decision on concrete integers.
Claim. For indices $(a,b,c,d,i,j)=(0,1,0,1,1,1)$ in $(\mathrm{Fin}\,4)^6$, the folded coupling numerator equals eight times the explicit table value: $N(0,1,0,1,1,1)=8\,Z(0,1,0,1,1,1)$.
background
In the 4D Regge exact-midpoint analysis, two integer-valued maps on sextuples of Fin 4 indices are compared. The numerator $N=m2Num$ is defined by folding a fixed coupling list: each term contributes via a local contrib kernel, and the fold starts at 0. The comparison target $Z=explicitZ$ is an explicit pattern-matched integer table on the same six indices (sample entries include $4$, $-2$, and so on for distinguished index patterns).
The local module is chunk 1 of a 256-way case split certifying $N=8Z$ at every point. Upstream, both $N$ and $Z$ live in the kernel-cert module; downstream assembly recombines the pointwise facts into a single universal statement.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values once the six Fin 4 arguments are fixed literals, so the kernel evaluates the fold defining $N$ and the pattern match defining $Z$ and checks equality with the factor 8. No lemmas are invoked beyond computational reduction.
why it matters
Feeds the parent assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N(a,b,c,d,i,j)=8Z(a,b,c,d,i,j)$ by nested fin_cases over all six indices. Each chunk entry such as this one discharges one concrete leaf of that case tree. In the gravity analysis stack this identity is the algebraic backbone equating the folded midpoint coupling numerator to a closed-form table, a step toward the exact 4D Regge midpoint M2TT identity. It is pure finite enumeration, not a continuum GR claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.