theorem sw_solution_bochner_constrains_fields {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) : sol.scalarCurvatureVal / 4 * sol.supNormSq + 1 / 4 * sol.supNormSq ^ 2 ≤ 0

Bochner-type constraint from the Seiberg-Witten equations. For any solution $(A, \psi)$, combining the Weitzenbock formula with $\|\nabla\psi\|^2 \ge 0$ yields $$\tfrac{s}{4}\,\|\psi\|^2_{\sup} + \tfrac{1}{4}\,\|\psi\|^4_{\sup} \le 0,$$ where $s$ is the (sampled) scalar curvature value.

theorem sw_solution_positive_scalar_forces_reducible {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) (hs : sol.scalarCurvatureVal > 0) : sol.supNormSq = 0

Positive scalar curvature forces $\psi \equiv 0$. If $s > 0$, then the Bochner constraint forces $\|\psi\|^2_{\sup} = 0$, so every SW solution is reducible. This is the analytic core of the vanishing of SW invariants on PSC manifolds.

theorem sw_solution_positive_scalar_is_reducible {M : Type u_1} [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 4)) M] {Ω1 : Type u_2} {Ω2 : Type u_3} [AddCommGroup Ω1] [Module ℝ Ω1] [AddCommGroup Ω2] [Module ℝ Ω2] {spinc : SpinCStructure M Ω1 Ω2} (sol : SWSolution spinc) (hs : sol.scalarCurvatureVal > 0) : sol.isReducible

Solutions on PSC manifolds are reducible. Combining the previous lemma with the reducibility characterization $\|\psi\|^2_{\sup} = 0 \iff \text{reducible}$: any SW solution on a manifold of positive scalar curvature is reducible.