Novikov Conjecture:invariance of higher signatures

### What is the conjecture
https://en.wikipedia.org/wiki/Novikov_conjecture

The Novikov Conjecture asserts that for any closed, oriented manifold $M$ with fundamental group $\pi_1(M)$, all of its higher signatures remain invariant under oriented homotopy equivalence.

Equivalently, via the Mishchenko–Fomenko and Kasparov formulations, tThe conjecture states that the topological K-theory assembly map

$$
K_\ast(B\pi_1(M)) \longrightarrow K_\ast(C_r^\ast(\pi_1(M)))
$$

is rationally injective.

This is one of the central open problems in topology and noncommutative geometry, connected to the Baum–Connes conjecture, positive scalar curvature, and rigidity theory.

---

### Prerequisites needed

Since the full analytic machinery is not yet available in mathlib, the conjecture can be included using abstract placeholders such as:

```lean
constant NovikovConjecture (G : Type _) [Group G] : Prop
```

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-XX

### Choose either option
- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reviewing the repository's conventions for adding formal conjecture statements and the proposed abstract `NovikovConjecture (G : Type _) [Group G] : Prop` declaration. Done means the Novikov Conjecture is added in the repository's expected form and its declaration is accepted by the relevant Lean checks.

Written by the indexing model from the issue text.