baum_connes_conjecture

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result baum_connes_conjecture is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Baum–Connes conjecture: For a countable group G, the K-theory of the reduced group C*-algebra Cr*(G) is isomorphic to the equivariant K-homology of the classifying space for proper G-actions, via the assembly map. Proved for many groups (amenable, hyperbolic, etc.); open in full generality.

Why this node was retired

The posted statement is

import Mathlib

theorem baum_connes_conjecture (G : Type*) [Group G] [Countable G]
    (hG : ∀ g : G, ∀ n : ℕ, g ^ n = 1 → n = 0 ∨ g = 1) :
    ∀ (n : ℤ),
      ∃ (idx : ℕ), idx = 0 ∨
        ∀ T : lp (fun _ : G => ℂ) 2 →L[ℂ] lp (fun _ : G => ℂ) 2,
          True := by
  sorry

The goal is ∀ (n : ℤ), ∃ (idx : ℕ), idx = 0 ∨ ∀ T, True, and the right disjunct is True, so idx = 0 need never hold and the statement is closed immediately. No assembly map, no K-theory and no group C*-algebra appear.

What a faithful statement would require

The assembly map from the equivariant K-homology of the classifying space for proper actions to the K-theory of the reduced group C*-algebra must be defined, and the conclusion must be that it is an isomorphism.

No corrected replacement node exists yet.