e_313003
plain-language theorem explainer
For the six-index tuple (3,1,3,0,0,3) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite it as one atomic cell in the 4D Regge midpoint M2TT identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a{=}3$, $b{=}1$, $c{=}3$, $d{=}0$, $i{=}0$, $j{=}3$ in $\mathrm{Fin}\,4$, the folded coupling numerator $N(a,b,c,d,i,j)$ equals $8$ times the explicit 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 $N$ (Lean m2Num) is the fold of a fixed coupling list: it sums a local contribution at each coupling triple. The closed form $Z$ (Lean explicitZ) is a sparse pattern-matched table of small integers (entries such as $4$, $-2$, and defaults).
The module is chunk 13 of a 256-cell decide grid that discharges $N=8Z$ pointwise. The ambient claim is the exact midpoint M2TT identity in four dimensions: after all index cases, the folded numerator is identically eight times the explicit kernel.
Upstream, only the two kernel definitions are needed; no analytic lemma intervenes at this cell.
proof idea
One-line decide on fully concrete Fin-4 indices. Both sides reduce to closed integers (the fold over the coupling list versus the pattern match in the explicit table), and the kernel checks equality. No rewrite lemmas or induction.
why it matters
Feeds the assembler m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4$, $N=8Z$ by exhaustive fin_cases. That global identity is the algebraic backbone of the Regge exact-midpoint M2TT certificate in 4D gravity analysis inside Recognition Science.
The factor of eight matches the eight-tick octave structure (T7) that organizes discrete recognition ticks; here it appears as a pure combinatorial multiplier between the folded coupling sum and the sparse kernel table. Closing every chunk cell removes scaffolding from the gravity side of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.