A sharp converse fractional-binomial inequality through log-convexity

We prove the converse fractional-binomial inequality posed by Gerhold and Simon as Conjecture 3.2, together with a biased refinement and optimality of the coefficient. Log-convexity of a finite sum of scaled Gamma quotients and its values at parameters one and two give the comparison. The Gamma-convexity ingredient is classical and explicitly credited. The Lean certificate covers the precise source statement, refinement and sharpness. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review. The accompanying Lean certificate covers the precise scoped main statement; inspect the formal endpoint, assumptions and provenance in the supporting package. Prior-art investigations are documented bounded searches, not worldwide-priority certification. Original prose is offered under CC BY 4.0 and original code/Lean under MIT; third-party rights and existing notices are preserved. The public supporting ZIP contains original proof sources and verification evidence, with bibliographic links and hashes instead of redistributed third-party source manuscripts. Recorded prior-art/source-access limits: No prior full sharp finite-sum resolution located. Alzer full article inaccessible; exact classical summand theorem and corollary types checked in two accessible primary successors. Absolute worldwide priority not certified.