A generic ray direction for finite planar data

Multiplication by a nonzero complex number makes the heights of every two distinct points in a prescribed finite set different. The multiplier is constructed by avoiding finitely many forbidden real slopes; no rational-coordinate or existing generic-position assumption is used. In particular, every nondegenerate segment with ends in the set becomes nonhorizontal. This is an original finite-avoidance argument.

theorem Cslib.Polygonal.exists_mul_im_injOn (s : Finset ℂ) : ∃ (u : ℂ), u ≠ 0 ∧ Set.InjOn (fun (z : ℂ) => (u * z).im) ↑s

A complex rotation and positive scaling separates the heights of all distinct points of any finite set. Coincident listed occurrences require no separation and remain coincident.