Mathematical proof that viscous damping always diminishes energy

In S. Coleman's The Fate Of the False Vacuum I he imagines a particle in a negative potential with "Euclidean" Lagrangian:

$$\frac{1}{2} \left(\frac{d \phi}{d \rho}\right)^2 + U$$

after Wick-rotation. This Lagrangian obeys the equation of motion:

$$\frac{d^2 \phi}{d \rho^2} + \frac{3}{\rho} \frac{d \phi}{d \rho} = \frac{dU}{d\phi}\tag{3.7}$$

where the $$\frac{3}{\rho}\frac{d\phi}{d\rho}$$ term acts as a damping force on the system. Qualitatively I understand that this always acts to decrease the energy of the system but I'm having trouble proving it mathematically. Through rearranging the second equation and multiplying through I can get to:

$$\frac{d \phi}{d \rho} \frac{d^2 \phi}{d \rho^2} - \frac{dU}{d \rho} = -\frac{3}{\rho} \left(\frac{d \phi}{d \rho}\right)^2.$$

In the paper, Coleman ultimately gets to the equation:

$$\frac{d}{d\rho}\left[\frac{1}{2} \left(\frac{d \phi}{d \rho}\right)^2 - U\right] = -\frac{3}{\rho} \left(\frac{d \phi}{d \rho}\right)^2 <0\tag{3.11}$$

to mathematically show that the damping force always leads to a loss of energy. What step am I missing to prove this? Where does the factor of $$\frac{1}{2}$$ come from and how is the Lagrangian related?

• You mean, where does $1/2$ in the expression for kinetic energy comes from? - mostly historical convention in defining mass. As for the proof: the derivative of a quantity is always negative, hence the quantity always decreases. I believe though that there is a sign error somewhere. Commented Jul 24 at 14:54
• A more familiar form in mechanics is $\frac{d}{dt}\left[\frac{mv^2}{2}+U(x)\right]=-\nu \frac{mv^2}{2}$, arizing from Newton's equation $m\ddot{x}=-\nu \dot{x}-\frac{d}{dx}U(x)$. Commented Jul 24 at 15:00
• Using the chain rule: $$\frac{d}{d\rho}\left[\frac{1}{2}\left(\frac{d\phi}{d\rho}\right)^2\right] = \frac{1}{2} \times \left(2 \frac{d\phi}{d\rho}\right) \times \frac{d}{d\rho} \frac{d\phi}{d\rho} = \frac{d\phi}{d\rho}\frac{d^2\phi}{d\rho^2}$$ More generally it's a weirdly useful trick that $u \frac{du}{dt} = \frac{1}{2} \frac{d u^2}{dt}$. Commented Jul 24 at 15:22

So this is a very standard thing that also happens in the work-energy theorem; we start with forces $$\mathbf F_i$$ and define the power that they exert through the trajectory $$\mathbf r(t)$$ as $$P_i=\mathbf F_i\cdot\dot{\mathbf r},$$then we come to Newton’s equations of motion that$$m\ddot{\mathbf r}=\sum_i \mathbf F_i,$$and after we multiply through by $$\dot{\mathbf r}$$ we argue that the left hand side is ultimately $$m\ddot{\mathbf r}\cdot\dot{\mathbf r}=\frac{\mathrm d\phantom{t}}{\mathrm dt}\left(\frac12m\dot{\mathbf r}\cdot\dot{\mathbf r}\right)=\frac{\mathrm dK}{\mathrm dt}.$$ What is the justification, here?
Two approaches. The first is to just take the derivative of the expression in the middle there, using the product rule (or, with a normal product like you have, you can instead use the chain rule). And if you take that derivative you will find the expression on the left hand side, and then you use the subtle but powerful fact that if $$B=A$$ then $$A=B$$: in other words in mathematics the equal sign does not have direction, if two things are equal they are just alternate ways of calculating the same number and you can take any expression containing one and substitute it with the other.
If that seems too easy or unsatisfying to you, Feynman used to brag about how he had one trick over all of his other classmates, which was to do everything under the integral sign. If you pause to integrate the expression and see what comes out you'll have a kind of abstract $$X(t) = \int_0^t\mathrm d\tau~ \ddot{\mathbf r}(\tau)\cdot\dot{\mathbf{r}}(\tau),$$with the promise that $$\frac{\mathrm d X}{\mathrm dt}$$ shall give you the sorts of expressions you we interested in above.
Once this is in an integral sign, we can integrate by parts, raising $$\ddot{\mathbf r}(\tau)$$ and lowering $$\dot{\mathbf r}(\tau)$$, to find that we end up almost where we started, but with a minus sign: $$X(t) = \big[ \dot{\mathbf r}(\tau)\cdot\dot{\mathbf{r}}(\tau)\big]_0^t-X(t).$$Collecting like terms on the left we can easily see$$2X = \big(\dot{\mathbf{r}}(t)\cdot\dot{\mathbf{r}}(t)\big)-\dot{\mathbf{r}}_0^2.$$ When I was a student this version saved me because for some reason I was really resistant to this idea that if $$B=A$$ then $$A=B$$. (To give a fuller explanation of my concern for those who don't see why: when you are manipulating equations, you sometimes have operations you can do that are like multiplying both sides by zero: they are technically valid and the equation that you get is technically valid, but the step is not invertible. So you want to prove X=Y but you have a justification that X=Z, if you start from your expression for Y and try to manipulate it into Y=Z, that derivation is only correct if all steps you took along that process were invertible. And in this context every equal sign starts to have a direction by convention, you can derive this from that but you might not be able to derive that from this.)