1 Scope, conventions, and prerequisites

1.1 The version of the conjecture

The main target is the Baum–Connes conjecture for all countable discrete groups, without coefficients, using the reduced group \(C^*\)-algebra. The degree is \(i\in \{ 0,1\} \). All algebras and Hilbert spaces are complex. Write \(\Gamma \) for a variable group; no particular matrix group is built into the definitions.

1.2 Standing assumptions

The group algebra, the regular representation, and the reduced group \(C^*\)-algebra make sense for arbitrary discrete groups. Impose countability for the main conjecture and the chosen separable KK-theoretic route. Specify all local compactness, Hausdorffness, and second-countability assumptions on spaces where they are needed.

1.3 Background interfaces

Organize prerequisites for Hilbert spaces, bounded operators, complex \(C^*\)-algebras (including nonunital algebras), functions vanishing at infinity, gradings, and filtered colimits of abelian groups.

1.4 Status conventions

The blueprint records verified foundations alongside later targets. Nodes marked as not ready are specifications to expand. Lean verification covers the reduced group \(C^*\)-algebra foundations and the operator \(K\)-theory constructions used in the comparisons below, including nonunital algebras and both degrees. Chapter 4 verifies the universal proper-space construction for countable discrete groups. Chapter 5 verifies the full even/odd equivariant KK groups, Kasparov product existence and laws, and natural comparisons with ordinary operator \(K_0\) and \(K_1\), under the stated separability and universe hypotheses. Its verification record documents the source corrections and exact Lean declarations. Chapter 6 verifies the actual topological \(K\)-homology colimit, its transition laws, cofinal indexing and universal proper-model independence, with the stated local compactness, second-countability and universe hypotheses. Chapter 7 constructs reduced Kasparov descent in both degrees, with full arbitrary interval homotopy transport and all four native Kasparov products. Its cutoff classes define the actual coefficient-free reduced assembly homomorphisms in degrees zero and one for countable discrete groups, with cofinal indexing and universal proper-model compatibility under the stated hypotheses; the general Baum–Connes conjecture is not proved here. Separate construction of the objects, formalization of the conjecture’s statement, and proof of the conjecture.