[proofplan]
The proof passes the limiting discrete energy-dissipation estimate for the minimizing-movement scheme to the limit. First, the assumed prelimit inequality supplies the endpoint energy balance together with the discrete metric-speed and local-slope dissipation terms. Then the endpoint convergence identifies the limiting endpoint energies. Finally, the two assumed lower semicontinuity inequalities for the metric-speed and slope terms give the continuum energy dissipation inequality.
[/proofplan]
[step:Record the limiting discrete energy-dissipation estimate]
Fix $0\le s\le t\le T$. By hypothesis, the discrete interpolations satisfy the limiting endpoint-form energy-dissipation estimate
\begin{align*}
\limsup_{n\to\infty}\left(\mathcal F[\bar\rho_{\tau_n}(t)]+\frac12\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r)-\mathcal F[\bar\rho_{\tau_n}(s)]\right)\le0.
\end{align*}
Equivalently, if
\begin{align*}
A_n:=\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)
\end{align*}
and
\begin{align*}
B_n:=\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r),
\end{align*}
then
\begin{align*}
\limsup_{n\to\infty}\left(\mathcal F[\bar\rho_{\tau_n}(t)]+\frac12A_n+\frac12B_n-\mathcal F[\bar\rho_{\tau_n}(s)]\right)\le0.
\end{align*}
[guided]
Fix $0\le s\le t\le T$. The statement assumes the limiting discrete energy-dissipation estimate in endpoint form:
\begin{align*}
\limsup_{n\to\infty}\left(\mathcal F[\bar\rho_{\tau_n}(t)]+\frac12\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r)-\mathcal F[\bar\rho_{\tau_n}(s)]\right)\le0.
\end{align*}
This is the form needed for passage to the limit at arbitrary fixed times $s$ and $t$. It avoids asserting a pointwise-in-$n$ inequality with the piecewise constant endpoints $\bar\rho_{\tau_n}(s)$ and $\bar\rho_{\tau_n}(t)$, which need not be valid when $s$ and $t$ lie inside time steps.
Define
\begin{align*}
A_n:=\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)
\end{align*}
and
\begin{align*}
B_n:=\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r).
\end{align*}
Both $A_n$ and $B_n$ belong to $[0,\infty]$ because they are integrals of nonnegative functions. With this notation, the assumed estimate is
\begin{align*}
\limsup_{n\to\infty}\left(\mathcal F[\bar\rho_{\tau_n}(t)]+\frac12A_n+\frac12B_n-\mathcal F[\bar\rho_{\tau_n}(s)]\right)\le0.
\end{align*}
[/guided]
[/step]
[step:Pass the endpoint energies to the limit]
For the fixed pair $0\le s\le t\le T$ chosen above, by the convergence assumption on the piecewise constant interpolations, applied at the fixed times $s$ and $t$,
\begin{align*}
\mathcal F[\bar\rho_{\tau_n}(s)]\to E(s)
\end{align*}
and
\begin{align*}
\mathcal F[\bar\rho_{\tau_n}(t)]\to E(t).
\end{align*}
Therefore the endpoint terms in the discrete inequality converge to the endpoint terms in the asserted continuum inequality.
[/step]
[step:Use lower semicontinuity for the metric-speed and slope terms]
Set
\begin{align*}
A_n:=\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)
\end{align*}
and
\begin{align*}
B_n:=\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r).
\end{align*}
The endpoint convergence and the assumed limiting discrete inequality give
\begin{align*}
E(t)+\frac12\liminf_{n\to\infty}(A_n+B_n)\le E(s).
\end{align*}
Since $A_n\ge0$ and $B_n\ge0$ for every $n\in\mathbb N$, the superadditivity of the lower limit for nonnegative extended-real sequences gives
\begin{align*}
\liminf_{n\to\infty}(A_n+B_n)\ge \liminf_{n\to\infty}A_n+\liminf_{n\to\infty}B_n.
\end{align*}
Therefore
\begin{align*}
E(t)
+\frac12\liminf_{n\to\infty}\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r)
+\frac12\liminf_{n\to\infty}\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r)
\le E(s).
\end{align*}
By the assumed lower semicontinuity of the metric derivative term,
\begin{align*}
\int_s^t |\rho'|^2(r)\,d\mathcal L^1(r)\le \liminf_{n\to\infty}\int_s^t |\rho_{\tau_n}'|^2(r)\,d\mathcal L^1(r).
\end{align*}
By the assumed lower semicontinuity of the relaxed-slope term,
\begin{align*}
\int_s^t G^2(\rho(r))\,d\mathcal L^1(r)\le \liminf_{n\to\infty}\int_s^t |\partial\mathcal F|^2(\tilde\rho_{\tau_n}(r))\,d\mathcal L^1(r).
\end{align*}
Substituting these two bounds into the lower-limit inequality yields
\begin{align*}
E(t)+\frac12\int_s^t |\rho'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t G^2(\rho(r))\,d\mathcal L^1(r)\le E(s).
\end{align*}
[/step]
[step:Conclude the energy dissipation inequality on every subinterval]
The preceding argument was carried out for an arbitrary pair $0\le s\le t\le T$. Hence the inequality
\begin{align*}
E(t)+\frac12\int_s^t |\rho'|^2(r)\,d\mathcal L^1(r)+\frac12\int_s^t G^2(\rho(r))\,d\mathcal L^1(r)\le E(s)
\end{align*}
holds for every $0\le s\le t\le T$. This is exactly the asserted energy dissipation inequality for the limit curve $\rho$ with relaxed slope $G$.
[/step]
