e_320330
plain-language theorem explainer
For the fixed multi-index (3,2,0,3,3,0) on Fin 4, the folded coupling numerator equals eight times the explicit integer kernel. Gravity analysts cite it when assembling the full 4D Regge midpoint M2TT numerator identity. The proof is a single kernel decide on concrete integers.
Claim. For indices $a=3$, $b=2$, $c=0$, $d=3$, $i=3$, $j=0$ in $\{0,1,2,3\}$, the summed coupling numerator equals eight times the explicit integer kernel value at that sextuple: $N(3,2,0,3,3,0)=8\,Z(3,2,0,3,3,0)$.
background
In the 4D Regge exact-midpoint M2TT analysis, two integer-valued maps on sextuples of Fin 4 indices are compared. The numerator $N(a,b,c,d,i,j)$ is defined by folding a fixed coupling list and summing each term's contribution at those indices. The explicit kernel $Z$ is a closed-form case table on the same sextuples, returning small integers such as $4$, $-2$, and so on.
The local module is chunk 14 of a 256-way case split: each chunk discharges one concrete sextuple equality $N=8Z$ by kernel decision. Upstream, $N$ and $Z$ are the certified definitions imported from the kernel certificate module; the present file only evaluates them at fixed points.
proof idea
One-line computational proof: decide evaluates both sides at the concrete Fin 4 values $(3,2,0,3,3,0)$ and checks integer equality. No algebraic lemmas are invoked; the kernel reduces the fold that defines the numerator and the case table that defines the explicit kernel to bare integers, then confirms they match under the factor eight.
why it matters
This is one atomic cell in the exhaustive Fin 4 case grid that builds the global identity m2Num_eq_eight_explicitZ, which states $\forall a,b,c,d,i,j,, N=8Z$. The assembly theorem introduces all six indices and runs fin_cases on each; the chunk theorems such as this one supply the decided equalities the case split lands on.
In the broader Recognition gravity stack, the identity certifies that the midpoint M2TT numerator is exactly eight times a sparse explicit kernel, a bookkeeping step toward closed-form curvature and mass-ladder checks in the discrete geometric sector. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure 4D index algebra supporting the Regge analysis layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.