Largest subset of {1,...,N} with all pairwise products distinct: pin the constant in $F(N)$ (Erdős #425)

Let $F(N)$ denote the maximum possible size of a subset $A\subseteq\{1,\ldots,N\}$ such that all pairwise products $ab$ with $a<b$ (equivalently, all products of two distinct elements of $A$) are distinct — a multiplicative Sidon set. Erdős asked whether there is a constant $c$ with $$F(N)=\pi(N)+(c+o(1))N^{3/4}(\log N)^{-3/2},$$ where $\pi$ is the prime-counting function. More generally, for an integer $r\geq 2$, if $A\subseteq\{1,\ldots,N\}$ is such that all products $a_1\cdots a_r$ with $a_1<\cdots<a_r$ (over $r$-element subsets) are distinct, is it true that $$\lvert A\rvert\leq \pi(N)+O\!\left(N^{\frac{r+1}{2r}}\right)?$$

Acceptance. FULLY RESOLVES (proof-shaped): a complete proof that determines the constant — establishing $F(N)=\pi(N)+(c+o(1))N^{3/4}(\log N)^{-3/2}$ with an explicit value of $c$ (in particular that the limit defining $c$ exists), or proving no such single constant exists; and/or a proof of the $r$-fold upper bound $\lvert A\rvert\leq\pi(N)+O(N^{(r+1)/(2r)})$. A machine-checkable proof (Lean/Coq) is preferred, otherwise a complete rigorous written proof; a numerical computation alone cannot close this. ADVANCES (each independently checkable): (a) replace the background's mere existence of $0<c_1\leq c_2$ by explicit numerical constants, or narrow the ratio $c_2/c_1$, with proof; (b) prove the $r$-fold bound for a specific value of $r$ where it was not previously known; (c) compute exact values of $F(N)$ over a stated range of $N$ with a reproducible search program and an exhaustiveness certificate, extending the known tabulated values and giving data-driven estimates of $c$. Deliver the proof, or the search code plus the certified table of $F(N)$ values.