Product-free sets in the free group

We prove that product-free sets of the free group over a finite alphabet have maximum density $1\mathrm{/}2$ with respect to the natural measure that assigns total weight one to each set of irreducible words of a given size. This confirms a conjecture of Leader, Letzter, Narayanan and Walters. In more general terms, we actually prove that strongly $k$-product-free sets have maximum density $1\mathrm{/}k$ in terms of the said measure.