e_300120
plain-language theorem explainer
For the single multi-index (3,0,0,1,2,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D midpoint M2–TT identity. The proof is a pure kernel decide on that fixed tuple.
Claim. Let $a,b,c,d,i,j\in\{0,1,2,3\}$. Writing $N$ for the folded coupling numerator and $Z$ for the explicit integer kernel, one has $N(3,0,0,1,2,0)=8\,Z(3,0,0,1,2,0)$.
background
In the 4D Regge midpoint analysis the numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list: each term contributes an integer depending on the six Fin-4 indices, and the fold starts from 0. The companion map $Z$ is an explicit piecewise-integer kernel on the same six indices (sample values include $4$, $-2$, and so on for listed patterns).
The local module is one of several decide-chunks whose sole job is to verify $N=8Z$ on a block of concrete index tuples. The parent assembly theorem then quantifies over all of Fin 4 by exhaustive fin_cases, invoking each chunk equality in turn.
Upstream, $N$ and $Z$ live in the kernel-certificate module; this chunk only specialises them at (3,0,0,1,2,0).
proof idea
One-line computational proof: decide evaluates both sides of the integer equality at the concrete Fin-4 sextuple and confirms they match. No lemmas are invoked beyond the definitions of the folded numerator and the explicit kernel.
why it matters
The declaration is a single cell in the 256-case kernel table that establishes $N=8Z$ pointwise. Downstream, m2Num_eq_eight_explicitZ assembles every such cell by nested fin_cases, obtaining the universal identity used in the Regge exact-midpoint M2–TT analysis. Without the chunk equalities the assembly proof has nothing to discharge. The result is pure discrete gravity bookkeeping inside the Recognition Science gravity stack; it does not itself touch the T0–T8 forcing chain or the continuum constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.