@[implicit_reducible]

noncomputable instance polyHasPositivity : HasPositivity (PolyΩ 0)

HasPositivity instance on degree-$0$ polynomial forms: a polynomial is positive iff it is a positive real constant.

@[reducible, inline]

abbrev E4Model : Type

Model 4-dimensional Euclidean space $\mathbb{R}^4$, used as a charted space target for 4-manifolds.

@[implicit_reducible]

noncomputable instance trivialHas4ManifoldTopology : Has4ManifoldTopology E4Model

Trivial Has4ManifoldTopology instance on $\mathbb{R}^4$ with all intersection-form invariants ($b_2$, signature) set to zero and Euler characteristic $2$.

noncomputable def trivialSymplecticManifold : SymplecticManifold TrivialΩ TrivialVF

Trivial symplectic manifold structure on the singleton differential-form scaffolding.

noncomputable def trivialSpinC : SpinCStructure E4Model PUnit.{u_1 + 1} PUnit.{u_2 + 1}

Trivial $\mathrm{Spin}^{\mathbb{C}}$ structure on $\mathbb{R}^4$ with spinor bundles $S^\pm = \mathbb{C}$ and zero curvature data; provides a concrete witness for the abstract API.