[proofplan]
The Hilbert field identities make the preferred field velocity $q(x,y)$ compatible with the derivative of the Hamilton-Jacobi potential $S$. For each competitor, the Weierstrass excess identity decomposes the Lagrangian into the total derivative of $S(x,y(x))$ plus a nonnegative remainder. Integration leaves only the fixed endpoint contribution and the excess integral, so every competitor has action at least the action of the characteristic $y_0$. Under strict excess positivity, equality forces the competitor to solve the same characteristic initial value problem as $y_0$, and the stated uniqueness hypothesis identifies it with $y_0$.
[/proofplan]
[step:Decompose the competitor integrand into a total derivative and excess]
Let $y\in C^1([a,b];U)$ be an admissible competitor. Define the field velocity along $y$ as the map $Q:[a,b]\to V$ given by
\begin{align*}
Q(x):=q(x,y(x)).
\end{align*}
The definition of $E$ gives
\begin{align*}
L(x,y(x),y'(x))=L(x,y(x),Q(x))+\partial_vL(x,y(x),Q(x))\cdot(y'(x)-Q(x))+E(x,y(x),y'(x)).
\end{align*}
The first Hilbert field identity gives
\begin{align*}
\partial_vL(x,y(x),Q(x))=\nabla_yS(x,y(x)).
\end{align*}
The second Hilbert field identity gives
\begin{align*}
L(x,y(x),Q(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot Q(x).
\end{align*}
Substituting these two identities into the excess decomposition yields
\begin{align*}
L(x,y(x),y'(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot y'(x)+E(x,y(x),y'(x)).
\end{align*}
Since $S$ extends to a $C^2$ map near the graph of $y$ and $y$ is $C^1$, the chain rule applies to the map $x\mapsto S(x,y(x))$ and gives
\begin{align*}
\frac{d}{dx}S(x,y(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot y'(x).
\end{align*}
Therefore
\begin{align*}
L(x,y(x),y'(x))=\frac{d}{dx}S(x,y(x))+E(x,y(x),y'(x)).
\end{align*}
[guided]
The goal is to compare the actual velocity $y'(x)$ with the field velocity selected by the Hamilton-Jacobi data. Define $Q:[a,b]\to V$ by $Q(x)=q(x,y(x))$. This map is well-defined because the graph of $y$ lies in $D$ and $q:D\to V$. The Weierstrass excess identity is exactly
\begin{align*}
L(x,y(x),y'(x))=L(x,y(x),Q(x))+\partial_vL(x,y(x),Q(x))\cdot(y'(x)-Q(x))+E(x,y(x),y'(x)).
\end{align*}
Now use the two Hilbert identities. The momentum identity gives
\begin{align*}
\partial_vL(x,y(x),Q(x))=\nabla_yS(x,y(x)).
\end{align*}
The Hamilton-Jacobi identity along the field gives
\begin{align*}
L(x,y(x),Q(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot Q(x).
\end{align*}
Substituting both formulas into the excess identity cancels the terms involving $Q(x)$:
\begin{align*}
L(x,y(x),y'(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot y'(x)+E(x,y(x),y'(x)).
\end{align*}
The differentiability hypotheses were included precisely so that the chain rule is legitimate along the curve. Because $S$ extends to a $C^2$ map near the graph of $y$ and $y$ is $C^1$, the map $x\mapsto S(x,y(x))$ is $C^1$ and
\begin{align*}
\frac{d}{dx}S(x,y(x))=\partial_xS(x,y(x))+\nabla_yS(x,y(x))\cdot y'(x).
\end{align*}
Hence the competitor integrand decomposes as
\begin{align*}
L(x,y(x),y'(x))=\frac{d}{dx}S(x,y(x))+E(x,y(x),y'(x)).
\end{align*}
[/guided]
[/step]
[step:Integrate the decomposition and use nonnegativity]
The decomposition from the previous step is an identity between continuous functions on $[a,b]$. Integrating it with respect to $\mathcal{L}^1$ gives
\begin{align*}
J[y]=\int_a^b \frac{d}{dx}S(x,y(x))\,d\mathcal{L}^1(x)+\int_a^b E(x,y(x),y'(x))\,d\mathcal{L}^1(x).
\end{align*}
The [fundamental theorem of calculus](/theorems/632) applies because $x\mapsto S(x,y(x))$ is $C^1$, so
\begin{align*}
\int_a^b \frac{d}{dx}S(x,y(x))\,d\mathcal{L}^1(x)=S(b,y(b))-S(a,y(a)).
\end{align*}
Using the endpoint conditions $y(a)=A$ and $y(b)=B$, we obtain
\begin{align*}
J[y]=S(b,B)-S(a,A)+\int_a^b E(x,y(x),y'(x))\,d\mathcal{L}^1(x).
\end{align*}
The excess is nonnegative on every admissible velocity, hence
\begin{align*}
J[y]\ge S(b,B)-S(a,A).
\end{align*}
[/step]
[step:Evaluate the endpoint expression on the characteristic curve]
For the reference curve $y_0$, the characteristic equation gives
\begin{align*}
y_0'(x)=q(x,y_0(x)).
\end{align*}
By the definition of $E$,
\begin{align*}
E(x,y_0(x),y_0'(x))=E(x,y_0(x),q(x,y_0(x)))=0
\end{align*}
for every $x\in[a,b]$. Applying the integrated decomposition to $y_0$ therefore gives
\begin{align*}
J[y_0]=S(b,B)-S(a,A).
\end{align*}
Together with the lower bound for an arbitrary competitor, this proves
\begin{align*}
J[y]\ge J[y_0].
\end{align*}
Thus $y_0$ is a minimizer in the stated competitor class.
[/step]
[step:Use strict excess positivity to identify equality cases]
Assume now that the excess is strictly positive away from the field velocity and that the characteristic initial value problem through $(a,A)$ has at most one admissible solution. Let $y$ be a competitor with $J[y]=J[y_0]$. The integrated decomposition gives
\begin{align*}
\int_a^b E(x,y(x),y'(x))\,d\mathcal{L}^1(x)=0.
\end{align*}
The integrand $x\mapsto E(x,y(x),y'(x))$ is continuous and nonnegative on $[a,b]$. A continuous nonnegative function on a compact interval with zero [Lebesgue integral](/page/Lebesgue%20Integral) must vanish everywhere. Therefore
\begin{align*}
E(x,y(x),y'(x))=0
\end{align*}
for every $x\in[a,b]$. Strict excess positivity then forces
\begin{align*}
y'(x)=q(x,y(x))
\end{align*}
for every $x\in[a,b]$. Since $y(a)=A$, the curve $y$ solves the same characteristic initial value problem as $y_0$ and has graph in $D$. The uniqueness hypothesis gives $y=y_0$ on $[a,b]$. Hence $y_0$ is the unique minimizer.
[/step]