My reasoning (as mathematical statements, as opposed to as snippets of Stan code) was that
\begin{alignat}{2}
&& D_1/d &\sim \mathcal{LN}(0,\sigma) \\
&\iff\qquad & \log(D_1/d) &\sim \mathcal{N}(0,\sigma) \\
&\iff\qquad & \log D_1 - \log d &\sim \mathcal{N}(0,\sigma) \\
&\iff\qquad & \log D_1 &\sim \mathcal{N}(\log d,\sigma) \\
&\iff\qquad & D_1 &\sim \mathcal{LN}(\log d,\sigma).
\end{alignat}
So I believe what I wrote was correct.
However, I did want to make a simple observation about my two models. One can check that the two likelihood functions implied by the two D2 ~ ... statements are numerically different (*). Hence, they define different probabilistic models. So both can’t be right! (And I assume version 1 is wrong and version 2 is right, but I want to think about it a bit more.)
(*) In fact, if n=1 then the model has two parameters: sigma and d[1], so one can plot the joint probability density as a heatmap. If one subtracts the densities from the two models one gets the plot below, which I thought was somewhat pretty.
