CLP Slice Rank Universal Exponential Ratio Strict Monotonicity

Proved

clp_slice_rank_universal_decay_1788790553

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

analysiscombinatoricserdos-problemsnumber-theory

For any tensor slice rank bound $C < N$ and dimensions $n_1 < n_2$ , the power-law ratio strictly decreases: $(C/N)^{n_2} < (C/N)^{n_1}$ .

Formal statement

import Mathlib

theorem clp_slice_rank_universal_decay_1788790553 (n1 n2 : ℕ) (hn : n1 < n2) (C N : ℝ)
    (hC_pos : 0 < C) (hC_lt : C < N) (hN_pos : 0 < N) :
    let r : ℝ := C / N
    (r ^ n2 < r ^ n1) ∧ (0 < r) := by sorry

View graph