Claims

../

2026_10_19_plasma_ai: Every set of $n$ reals contains a dissociated subset of size at least $\log_2n-\log_2(\log_2n+1)$, proved in Lean at tier 2, and of size at least $\log_2n-\log_2\log_2\log_2n-4$ for $n\ge2^{16}$, author-recorded at tier 0; the asked $\lfloor\log_2n\rfloor$ stays open, and catalog acceptance is pending.

---