e_021020
plain-language theorem explainer
For the six-index tuple (0,2,1,0,2,0) on Fin 4, the folded numerator m2Num equals eight times the closed-form kernel value explicitZ. Gravity analysts cite this as one atomic case in the 4D Regge midpoint M2 identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=0$, $b=2$, $c=1$, $d=0$, $i=2$, $j=0$ in $\mathrm{Fin}\,4$, the folded coupling numerator equals eight times the explicit integer kernel: $N(0,2,1,0,2,0)=8\,Z(0,2,1,0,2,0)$.
background
In the 4D Regge midpoint analysis, two integer-valued maps on six $\mathrm{Fin},4$ indices appear. The numerator $N=m2Num$ is obtained by folding a fixed coupling list and summing a local contribution at each term. The companion map $Z=explicitZ$ is a sparse closed-form table of small integers (entries such as $4$, $-2$, and defaults) encoding the same kernel in closed form.
The module is chunk 2 of a 256-case decide grid that checks $N=8Z$ pointwise. The factor eight is the combinatorial normalization tying the folded sum to the explicit table. Upstream, both maps are defined in the kernel certificate module; this file only discharges individual index sextuples.
proof idea
One-line proof by decide. Both sides reduce to concrete Int values for the fixed indices $(0,2,1,0,2,0)$: the left via the fold definition of the numerator, the right via the pattern table for the explicit kernel scaled by eight. No lemmas beyond kernel evaluation are invoked.
why it matters
Feeds the assembly theorem m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$ by exhaustive fin_cases on all six indices. Each chunk lemma such as this one is a leaf in that case split. In the gravity stack this identity certifies that the midpoint M2 numerator matches the explicit 4D Regge kernel, a computational step toward the continuum limit identities used in the RS gravity analysis. It does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law; it is pure discrete kernel bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.