ICC criterion [connes-001J]
✍️source

    Theorem. Orbit and displacement criterion for ICC [connes-0006]
    isICC_of_product_quotientpaper_gammaOne_iccpaper_gammaTwo_icc
    L∃∀N

      For a countable group, the ICC condition asks that every nonidentity conjugacy class be infinite. In a semidirect product \(N\rtimes (S\times Q)\), the proof can be separated from the concrete formulas by supplying two kinds of certificates:

      1. every nonidentity \(a\in N\) has an infinite \(S\)-orbit; and
      2. every nonidentity \(q\in Q\) admits \(a\in N\) whose displacement \(a(q\cdot a)^{-1}\) is nonidentity and has an infinite \(S\)-orbit.

      The structure Connes.PaperICC.ActionData is exactly this direct-consumer boundary. The generic theorem Connes.PaperICC.isICC_of_product_quotient then proves that these certificates imply ICC by splitting a nonidentity element into three exhaustive cases.

      • A nontrivial \(S\)-coordinate inherits an infinite conjugacy class from \(S\).
      • A pure kernel element uses the first certificate.
      • A surviving \(Q\)-coordinate reduces to the second certificate.

      This organization follows the cases used in [zhou2026icc, Section 5] without building the concrete tensors into the reusable ICC theorem.

      References

        Reference. ICC property-(T) groups without W-star-superrigidity [zhou2026icc]

        @misc{zhou2026icc,
  title = {ICC Property-(T) Groups Without W*-Superrigidity},
  author = {Zhou, Shuoxing},
  year = {2026},
  eprint = {2608.02327},
  archivePrefix = {arXiv},
  primaryClass = {math.OA},
  url = {https://arxiv.org/abs/2608.02327}
}

        Context

          ICC by orbit displacement (Zhou §5) [connes-0014]

            ICC criterion [connes-001J]
            ✍️source

              Theorem. Orbit and displacement criterion for ICC [connes-0006]
              isICC_of_product_quotientpaper_gammaOne_iccpaper_gammaTwo_icc
              L∃∀N

                For a countable group, the ICC condition asks that every nonidentity conjugacy class be infinite. In a semidirect product \(N\rtimes (S\times Q)\), the proof can be separated from the concrete formulas by supplying two kinds of certificates:

                1. every nonidentity \(a\in N\) has an infinite \(S\)-orbit; and
                2. every nonidentity \(q\in Q\) admits \(a\in N\) whose displacement \(a(q\cdot a)^{-1}\) is nonidentity and has an infinite \(S\)-orbit.

                The structure Connes.PaperICC.ActionData is exactly this direct-consumer boundary. The generic theorem Connes.PaperICC.isICC_of_product_quotient then proves that these certificates imply ICC by splitting a nonidentity element into three exhaustive cases.

                • A nontrivial \(S\)-coordinate inherits an infinite conjugacy class from \(S\).
                • A pure kernel element uses the first certificate.
                • A surviving \(Q\)-coordinate reduces to the second certificate.

                This organization follows the cases used in [zhou2026icc, Section 5] without building the concrete tensors into the reusable ICC theorem.

                Formalizing the ICC criterion [connes-000X]
                isICC_of_product_quotientpaper_gammaOne_iccpaper_gammaTwo_icc
                L∃∀N

                  The paper-specific work behind Theorem [connes-0006] is confined to orbit calculations in ICCOrbits.lean. Those calculations construct the action data and yield Connes.PaperICC.paper_gammaOne_icc and Connes.PaperICC.paper_gammaTwo_icc.

                  The displacement certificate is the finite-quotient input. Conjugating an element with nontrivial \(Q\)-coordinate by a kernel element changes its kernel coordinate by \(a(q\cdot a)^{-1}\). Asking directly for an infinite family of conjugates would duplicate this algebra for each action. The certificate instead exposes the one displacement whose infinite \(S\)-orbit suffices.