Rational approximation to log₂ 3

We prove that the irrationality exponent of θ = log2 3 is at most three. For every ε > 0, every sufficiently large positive integer q, and every integer p, |θ − p/q| ≥ q−3−ε. The proof combines weighted interpolation at the points (2j, 3j), denominator clearing, and a joint estimate for auxiliary and Taylor indices. A curve inequality supplies the interpolation theorem. The proof is formalized in Lean. The deposit includes the paper, LaTeX sources, and Lean sources with pinned dependencies and reproduction instructions. Code: https://github.com/rohitkrjha/log23-measure The manuscript and original documentation are licensed under CC BY 4.0; original code is licensed under Apache 2.0. Third-party code retains its existing licenses.