Nonnegativity of \mathcal{S} follows directly from nonnegativity of s(\cdot,\cdot). Further, it follows from Lemma 5.2 that \mathrm{Val}(x_0)\in{\mathbb{R}} for all x_0\in\mathcal{X}.
The statement that \mathcal{S} is a bounded quadratic form will be proven in several steps.
Step 1: We show that \mathrm{Val}(\lambda x_0)=|\lambda|^2\mathrm{Val}(x_0) for all x_0\in\mathcal{X}, \lambda\in{\mathbb{C}}. The statement is clear for \lambda=0, so we can assume that \lambda\neq0 in the following.
Let x_0\in\mathcal{X} and \varepsilon>0. Then, by Lemma 5.2 and the definition of the value function, there exists a generalized trajectory (x(\cdot),u(\cdot),y(\cdot)) with x(0)=x_0 and
\mathcal{J}\bigl(y(\cdot),u(\cdot)\bigr)\leq \mathrm{Val}(x_0)+\frac{\varepsilon}{|\lambda|^2}.
Using that (\lambda x(\cdot),\lambda u(\cdot),\lambda y(\cdot)) is a generalized trajectory with \lambda x(0)=\lambda x_0, we obtain, by quadraticity of s,
\begin{gathered}
\mathrm{Val}(\lambda x_0)\leq \mathcal{J}(\lambda x(\cdot),\lambda u(\cdot))=|\lambda|^2\mathcal{J}( y(\cdot),u(\cdot))
= |\lambda|^2\,\mathcal{J}(y(\cdot),u(\cdot))\\
\leq |\lambda|^2\left(\mathrm{Val}(x_0)+\frac{\varepsilon}{|\lambda|^2}\right)
=|\lambda|^2\mathrm{Val}(x_0)+\varepsilon.
\end{gathered}
Since the latter holds for all \varepsilon>0, we have \mathrm{Val}(\lambda x_0)\leq |\lambda|^2 \mathcal{S}(x_0). Applying this with x_0 replaced by \lambda x_0 and with the factor 1/\lambda gives the reverse inequality, hence \mathrm{Val}(\lambda x_0)=|\lambda|^2\mathrm{Val}(x_0).
Step 2: We show the parallelogram identity
\forall\,x_{0,1},x_{0,2}\in\mathcal{X}:\quad \mathrm{Val}(x_{0,1}+x_{0,2})+\mathrm{Val}(x_{0,1}-x_{0,2})
=2\mathrm{Val}(x_{0,1})+2\mathrm{Val}(x_{0,2})
.
Let x_{0,1},x_{0,2}\in\mathcal{X} and \varepsilon>0. Then there exist generalized trajectories (x_i(\cdot),u_i(\cdot),y_i(\cdot)) with x_i(0)=x_{0,i} such that
\mathcal{J}\bigl(y_i(\cdot),u_i(\cdot)\bigr)\le\mathrm{Val}(x_{0,i})+\frac{\varepsilon}{4},
\qquad i=1,2.
Clearly, the sums and differences
(x_\pm(\cdot),u_\pm(\cdot),y_\pm(\cdot)):=\bigl(x_1(\cdot)\pm x_2(\cdot),\;u_1(\cdot)\pm u_2(\cdot),\;y_1(\cdot)\pm y_2(\cdot)\bigr)
are generalized trajectories with initial states x_{0,1}\pm x_{0,2}. Since s is quadratic, we have the integrand-level parallelogram identity, and hence
\mathcal{J}\bigl(y_+,u_+\bigr)+\mathcal{J}\bigl(y_-,u_-\bigr)
=2\mathcal{J}\bigl(y_1,u_1\bigr)+2\mathcal{J}\bigl(y_2,u_2\bigr).
Therefore,
\mathrm{Val}(x_{0,1}+x_{0,2})+\mathrm{Val}(x_{0,1}-x_{0,2})
\le2\,\mathrm{Val}(x_{0,1})+2\mathrm{Val}(x_{0,2})+\varepsilon.
Since \varepsilon>0 is arbitrary, we obtain
\mathrm{Val}(x_{0,1}+x_{0,2})+\mathrm{Val}(x_{0,1}-x_{0,2})
\le2\,\mathrm{Val}(x_{0,1})+2\mathrm{Val}(x_{0,2}).
For the reverse inequality, set \tilde x_{0,1}:=\tfrac12(x_{0,1}+x_{0,2}) and \tilde x_{0,2}:=\tfrac12(x_{0,1}-x_{0,2}). Applying the previous estimate to \tilde x_{0,1},\tilde x_{0,2} and using Step 1 with \lambda=\tfrac12, we get
\begin{gathered}
2\mathrm{Val}(x_{0,1})+2\mathrm{Val}(x_{0,2})
=4\mathrm{Val}(\tilde x_{0,1})+4\,\mathrm{Val}(\tilde x_{0,2})\\
\le\mathrm{Val}(x_{0,1}+x_{0,2})+\mathrm{Val}(x_{0,1}-x_{0,2}),
\end{gathered}
which proves the parallelogram identity.
Step 3: We conclude that \mathrm{Val} is a quadratic form. Indeed, Steps 1-2 verify the hypotheses of [Kurepa1965QSF, Thm. 1]; hence, by that theorem, (?) is a sesquilinear form. Thus \mathrm{Val}:\mathcal{X}\to{\mathbb{R}} is a quadratic form.
Step 4: We show that \mathrm{Val} is a bounded quadratic form. It can be concluded from Lemma 5.2 that, for M as in that lemma,
\forall\, x_0\in\mathcal{X}\text{ with }\norm{x_0}_\mathcal{X}\leq 1:\quad\mathrm{Val}(x_0)\leq M\,\norm*{\left[\begin{smallmatrix}Q & S\\S
\setcounter{i}{1}
\striche={\ast}
\loop
\ifnum\value{i}<1
\striche=\expandafter{\the\expandafter\striche\ast}
\stepcounter{i}
\repeat
^{\the\striche}
& R\end{smallmatrix}\right]}.
Hence, by using that \mathrm{Val} is quadratic, we have
\forall\, x_0\in\mathcal{X}:\quad\mathrm{Val}(x_0)\leq M\,\norm*{\left[\begin{smallmatrix}Q & S\\S
\setcounter{i}{1}
\striche={\ast}
\loop
\ifnum\value{i}<1
\striche=\expandafter{\the\expandafter\striche\ast}
\stepcounter{i}
\repeat
^{\the\striche}
& R\end{smallmatrix}\right]}\,\norm{x_0}_\mathcal{X}^2.
Assume that (x(\cdot),u(\cdot),y(\cdot)) is a classical trajectory on [0,T], T>0. We essentially follow the argument of the corresponding finite-dimensional proof in [Will71a]. For \varepsilon>0, let ({x}_1(\cdot),{u}_1(\cdot),{y}_1(\cdot)) be a generalized solution with {x}_1(0)=x(T) and
\mathcal{J}\bigl({y}_1(\cdot),{u}_1(\cdot)\bigr)\le\mathrm{Val}(x(T))+{\varepsilon}.
Now consider the concatenation of the two trajectories, defined by
(\tilde x(t),\tilde u(t),\tilde y(t))=
\begin{cases}
(x(t),u(t),y(t)), & 0\le t\le T,\\
\bigl(x_1(t-T),u_1(t-T),y_1(t-T)\bigr), & t> T,
\end{cases}
Then (\tilde x(\cdot),\tilde u(\cdot),\tilde y(\cdot)) is a generalized trajectory with \tilde u(\cdot)\in\mathrm{L}^{2}({\mathbb{R}}_{\ge0};\mathcal{U}) and \tilde y(\cdot)\in\mathrm{L}^{2}({\mathbb{R}}_{\ge0};\mathcal{Y}), whence
\begin{aligned}
\mathrm{Val}(x(0))&=\mathrm{Val}(\tilde{x}(0))\leq \mathcal{J}(\tilde{y}(\cdot),\tilde{u}(\cdot))\\&=\int_0^Ts\bigl(\tilde{y}(t),\tilde{u}(t)\bigr)\mathop{\frac{\text{\normalfont d}}{\text{\normalfont d}t}}+\int_0^\infty s\bigl(\tilde{y}(t+T),\tilde{u}(t+T)\bigr)\mathop{\frac{\text{\normalfont d}}{\text{\normalfont d}t}}\\
&=\int_0^Ts\bigl({y}(t),{u}(t)\bigr)\mathop{\frac{\text{\normalfont d}}{\text{\normalfont d}t}}+\mathcal{J}\bigl({y}_1(\cdot),{u}_1(\cdot)\bigr)\mathop{\frac{\text{\normalfont d}}{\text{\normalfont d}t}}\\
&\leq\int_0^Ts\bigl({y}(t),{u}(t)\bigr)\mathop{\frac{\text{\normalfont d}}{\text{\normalfont d}t}}+\mathrm{Val}(x(T))+\varepsilon.
\end{aligned}
Since this holds for all \varepsilon>0, we can conclude that the dissipation inequality holds.