The global $H^2$ estimate without the $L^2$ term under uniqueness

Assume the Axiom of Choice and Countable Choice. In the setting of Global $H^2$ Dirichlet regularity suppose that the homogeneous problem has only the trivial solution: $u\in H_0^1(\mathrm{\Omega })$ and $a(u,v)=0$ for all $v\in H_0^1(\mathrm{\Omega })$ imply $u=0$. Then for every $f\in L^2(\mathrm{\Omega })$ the unique weak solution $u\in H_0^1(\mathrm{\Omega })$ of $Lu=f$ satisfies $u\in H^2(\mathrm{\Omega })$ and there is $C=C(n,\mathrm{\Omega },\theta ,M_a,M_b,M_c,\mathrm{\parallel }D{a}^{ij}{\mathrm{\parallel }}_{\mathrm{\infty }},\mathrm{\parallel }{L}^{-1}{\mathrm{\parallel }}_{\mathcal{L}(L^2(\mathrm{\Omega }),H_0^1(\mathrm{\Omega }))})$ with $\mathrm{\parallel }u{\mathrm{\parallel }}_{H^2(\mathrm{\Omega })}\le C\mathrm{\parallel }f{\mathrm{\parallel }}_{L^2(\mathrm{\Omega })}\mathrm{.}$ Thus the $L^2$ term may be dropped exactly under the injectivity hypothesis, and the estimate is uniform over all data.

Hunter's Section 4.10 (printed pp. 106-110) proves the Fredholm alternatives for $Lu-\lambda u=f$ with the compact resolvent; the library's Fredholm page formalises them, and the corollary draws the standard consequence that a trivial kernel yields existence and a bounded solution map, which removes the $L^2$ term of the global $H^2$ estimate. The contradiction alternative via Rellich compactness recorded in the scaffold is subsumed by the formalised compactness statement of the Fredholm page.