[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*}[/step]

[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: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]