e_310322
plain-language theorem explainer
For the six Fin-4 indices (3,1,0,3,2,2), the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts assembling the 4D Regge midpoint M2TT identity cite this as one of the 256 kernel point checks. The proof is a single decide on concrete integers.
Claim. For indices $a=3$, $b=1$, $c=0$, $d=3$, $i=2$, $j=2$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit kernel integer: $N(3,1,0,3,2,2)=8\,Z(3,1,0,3,2,2)$.
background
In the 4D Regge midpoint analysis, two integer-valued kernels on six $\mathrm{Fin},4$ indices are compared. The numerator $N=m2Num$ is obtained by folding a fixed coupling list and summing local contributions at each multi-index. The comparison target $Z=explicitZ$ is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults) on the same index domain.
The module is chunk 13 of a 256-way partition of the kernel: each chunk discharges a block of concrete index tuples for the pointwise identity $N=8Z$. Upstream, $m2Num$ and $explicitZ$ are pure definitions in the kernel certificate module; no analytic hypotheses are attached.
The ambient goal is an exact algebraic identity used in the discrete gravity / Regge calculus side of the Recognition stack, not a continuum limit statement.
proof idea
One-line kernel decision: decide evaluates both sides at the fixed indices $(3,1,0,3,2,2)$ and checks integer equality. No lemmas are invoked beyond the reducibility of the fold defining $m2Num$ and the pattern match defining $explicitZ$.
why it matters
Feeds the assembler theorem $m2Num_eq_eight_explicitZ$, which states $\forall a,b,c,d,i,j\in\mathrm{Fin},4$, $m2Num=8\cdot explicitZ$ by exhaustive $fin_cases$ over all six indices. Each chunk theorem such as this one supplies one concrete case so the global identity is a pure case split rather than a symbolic summation argument.
In the gravity analysis layer this identity certifies that the folded coupling numerator is exactly eight times the explicit midpoint kernel, a bookkeeping step toward the Regge exact midpoint M2TT identity in 4D. It does not itself touch the forcing chain (T0–T8), $\phi$-ladder masses, or $\alpha$; it is infrastructure for the discrete curvature side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.