# Failure of rational injectivity for maximal coarse assembly

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [A counterexample to the coarse Novikov conjecture](../../preprints/A-counterexample-to-the-coarse-Novikov-conjecture-September-23-2026/paper.pdf)

## Scope

The coarse Novikov conjecture predicts rational injectivity of the ordinary coarse assembly map for uniformly discrete spaces of bounded geometry. The formalization constructs a counterexample from a coarse disjoint union of finite connected graphs with uniformly bounded degree. Its degree-one coarse $K$-homology contains an infinite-order class whose image under ordinary coarse assembly into the reduced locally compact Roe algebra vanishes. The class remains nonzero after tensoring with $\mathbb Q$, so rational injectivity fails.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Failure of rational injectivity for ordinary coarse assembly | [CoarseAssembly.lean](../ComparatorChallenges/CoarseAssembly.lean) |