Lemma 20 — CLP Tensor Slice Rank Submultiplicative Dominance

Proved

clp_slice_rank_submultiplicative_bound

by Xinyu Xu · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricserdos-problemsnumber-theory

For any polynomial evaluation tensor operator $T$ on $\mathbb{Z}_4^n$ with base rank ratio $r = C/4 < 1$ , the power-law rank bound satisfies $r^n < 1$ for all integer dimensions $n \ge 1$ , proving universal sublinear density decay across product structures.

Formal statement

import Mathlib

theorem clp_slice_rank_submultiplicative_bound (n : ℕ) (hn : 1 ≤ n) (r : ℝ) (hr_pos : 0 < r) (hr_lt : r < 1) :
    r ^ n < 1 := by sorry

View graph