Conditional formalization of Zhou's Connes-rigidity counterexample

Source: arxiv:2608.02327, url:https://github.com/utensil/connes-rigidity Authors: Utensil Song Status: verified Main declarations: Connes.theoremA Tags: operator-algebras, von-neumann-algebras, property-t, group-theory, connes-rigidity MSC: 46L10, 20F65, 22D10