An explicit irrationality-exponent bound for ζ(3) − rζ(2)

For every fixed rational number r, we prove 2 ≤ μ(ζ(3) − rζ(2)) ≤ 10,000. More precisely, every reduced rational approximant a/q of sufficientlylarge denominator satisfies |ζ(3) − rζ(2) − a/q| > q^(−10000). Thethreshold may depend on r. The proof extends Qian Tang's determinantconstruction using an exponential conditioning estimate for a positiveGram matrix, a normalized-slope estimate, and a bilinear determinantcomparison. A prime in a logarithmic interval then yields the denominatorbound. The final statements and their dependencies are verified in Lean.The exponent is not optimized, and no numerical denominator thresholdis computed. This record contains the manuscript PDF, its LaTeX source, and the Leanformalization with pinned dependency versions and reproduction instructions.