Unit-distance upper bound with exponent $4/3$

Read-back. The statement asserts the existence of at least one real number $C$ (not claimed to be unique, and no explicit value or bound on it is given) satisfying two conditions: first, $C>0$ (strict), and second, that for every finite set $P$ of points of $\mathbb{R}^2$ — formally, Finset (EuclideanSpace ℝ (Fin 2)), i.e. a finite set of functions $\mathrm{Fin}\,2\to\mathbb{R}$ carrying the Euclidean ($\ell^2$) metric, so that dist p q is the usual distance $\sqrt{(p_0-q_0)^2+(p_1-q_1)^2}$ — the inequality

holds, where $|P|$ is the number of elements of $P$, the left-hand side is the natural number unitDist(P) cast into $\mathbb{R}$, and the exponent $4/3$ is a real exponent applied to the nonnegative real $|P|$ (in particular $0^{4/3}=0$). The quantity unitDist(P) is defined by this bundle: form the set of ordered pairs $(p,q)$ with $p,q\in P$ and $p\neq q$, keep exactly those with distance equal to $1$, take the cardinality, and divide by $2$ using natural-number (truncating) division; hence it is the floor of half the number of such ordered pairs. Every finite $P$ is included with no side hypotheses: the empty set gives $0\le C\cdot0=0$, and singletons are included as well. The same single positive $C$ must work for all finite $P$; the inequality is non-strict ($\le$). Nothing is asserted about lower bounds, optimality of the exponent, constructions attaining the bound, or dimensions other than two. The declaration lives in namespace CrossingConsequences, and its proof is left as by sorry (no proof term is supplied).