---

Claim. A set $B$ of real numbers is dissociated if distinct finite subsets of $B$ have distinct sums, the empty subset with sum $0$ included; for a finite set $X\subset\mathbb R$ let $d(X)$ be the largest size of a dissociated subset of $X$, and let $f(n)$ be as in the problem.

First, every nonempty finite set $A\subset\mathbb R$ with $n$ elements contains a dissociated subset of size at least $\log_2n-\log_2(\log_2n+1)$, so

$$f(n)\ge\log_2n-\log_2(\log_2n+1)\qquad(n\ge1).$$

Second, every finite set $A\subset\mathbb R$ with $n=|A|\ge5$ satisfies

$$d(A)\ge\log_2(n-1)-\log_2\bigl(\lceil\log_2\log_2n\rceil+2+\sqrt2\bigr)-\log_26,$$

and consequently $f(n)\ge\log_2n-\log_2\log_2\log_2n-4$ for every $n\ge2^{16}$.

Third, a nonempty finite set $P$ of $n$ positive reals with $\max P\le\frac43\min P$ has $n\le2^{d(P)}-1$; in particular $d(P)\ge\lfloor\log_2n\rfloor$ for such sets.

Covers. The open-ended estimate of $f(n)$ asked by Problem 963: the lower bound rises from Erdős's greedy bound $\lfloor\log_3n\rfloor$ to $\log_2n-O(\log\log n)$ for every $n$, and to $\log_2n-\log_2\log_2\log_2n-4$ for $n\ge2^{16}$. The definite question, whether $f(n)\ge\lfloor\log_2n\rfloor$ for every $n$, stays open: the first bound lies strictly below $\lfloor\log_2n\rfloor$ for every $n\ge2$, the second does not decide it, and the third gives the asked bound only for positive sets whose largest element is at most $4/3$ times the smallest. No upper bound on $f(n)$ and no sharpness of these bounds is claimed.

Standing. The first bound is L22 at tier 2. Its Lean proof passes the axiom audit, depending only on propext, Classical.choice and Quot.sound with no compiler axiom, and the independent whole-statement fidelity audit and its distinct passing grade are filed on the card. The second and third bounds are L213 and L212 at tier 0: author-recorded by Plasma AI, with complete written proofs and no independent examination or Lean proof; they do not inherit L22's warrant. Catalog acceptance is pending.

Depends on. L22 (tier 2), L213 (tier 0) and L212 (tier 0), which L213 applies to each dyadic block of the absolute values.