Density $d_t$ of $n$ representing $t$ as a sum of distinct divisors: is $d_t\sim c_1(\log t)^{-c_2}$? (Erdős #859)

For an integer $t\geq 1$, let $d_t$ be the natural density of the set of integers $n\in\mathbb{N}$ for which $t$ can be represented as a sum of distinct divisors of $n$. (Erdős proved that this density exists for every $t$.) Do there exist constants $c_1,c_2>0$ such that $$d_t\sim\frac{c_1}{(\log t)^{c_2}}$$ as $t\to\infty$?

Acceptance. FULLY RESOLVES: prove or disprove the asymptotic $d_t\sim c_1/(\log t)^{c_2}$ — either exhibit constants $c_1,c_2>0$ and prove that $d_t(\log t)^{c_2}\to c_1$, or prove that no such pair exists (e.g. that $d_t(\log t)^{c}$ fails to converge to a positive limit for every $c>0$); machine-checkable (Lean/Coq) preferred, else a complete written proof. ADVANCES: (a) narrow the exponent gap — prove an upper bound $d_t<(\log t)^{-c_4'}$ with $c_4'$ strictly larger than, and/or a lower bound $d_t>(\log t)^{-c_3'}$ with $c_3'$ strictly smaller than, the best explicit exponents stated in the literature, with proof; (b) prove one-sided regular variation of $d_t$ — e.g. that $\log(1/d_t)/\log\log t$ converges to a limit (which would be the exponent $c_2$) — with proof; (c) reproducible high-range computation of $d_t$ that pins the empirical exponent $c_2$ to a certified numerical interval and tests the single-power hypothesis, with code and a convergence analysis. Deliver the proof file, or the computation code + certified estimates.