e_023103
plain-language theorem explainer
For the six-index tuple (0,2,3,1,0,3) on Fin 4, the folded numerator m2Num equals eight times the explicit kernel value explicitZ. Gravity analysts cite these pointwise identities when assembling the global Regge midpoint M2TT relation. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}0$, $b{=}2$, $c{=}3$, $d{=}1$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the tabulated explicit kernel entry: $N(0,2,3,1,0,3)=8\,Z(0,2,3,1,0,3)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six Fin-4 indices are compared. The numerator $N=m2Num$ is obtained by folding a fixed coupling list and summing local contributions at $(a,b,c,d,i,j)$. The comparison target $Z=explicitZ$ is a sparse explicit table of small integers (entries such as $4$, $-2$, and defaults).
The module is one chunk of a 256-case decide grid establishing the pointwise identity $N=8Z$. Chunk 2 covers a block of those index sextuples; the present declaration is the single cell $(0,2,3,1,0,3)$.
Upstream, $m2Num$ and $explicitZ$ are pure definitions in the kernel certificate module: the former is a fold, the latter a pattern-matched lookup. No analytic closed form is assumed here; equality is checked on concrete values.
proof idea
One-line proof by decide. Both sides reduce to concrete integers once the six Fin-4 arguments are fixed: the fold defining the numerator evaluates fully, and the explicit table returns a fixed Int. Lean’s kernel decision procedure discharges the resulting numeral equality. No lemmas beyond the two definitions are invoked.
why it matters
Feeds the assembler theorem $m2Num_eq_eight_explicitZ$, which states $\forall a,b,c,d,i,j., N=8Z$ by exhaustive fin_cases over Fin 4. That global identity is the algebraic content of the Regge-exact midpoint M2TT relation in 4D: the folded coupling numerator is exactly eight copies of the sparse kernel.
Within Recognition gravity, this sits in the discrete curvature/bookkeeping layer that supports continuum limits and effective Newtonian structure. It does not itself invoke the forcing chain (T5–T8) or the J-cost; it is pure finite combinatorial certification needed before continuum claims can be trusted.
Each chunk theorem closes one cell of the 256-case grid so the assembler can stay a thin case split rather than a monolithic decide.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.