Spatial factor equivalence [connes-001F]
✍️source

    Theorem. Spatial implementation of the factor equivalence [connes-0007]
    SpatialWitnessisNormaltracialEquiv_of_spatialWitnesspaperGroupFactors_isomorphic
    L∃∀N

      The group von Neumann algebra \(L(G)\) is represented on \(\ell ^2(G)\) as the von Neumann closure of the left regular operators. Its canonical trace is the vacuum coefficient at \(\delta _e\). Consequently a unitary \(U:\ell ^2(G)\simeq \ell ^2(H)\) gives the required tracial equivalence once two facts are proved: conjugation by \(U\) carries one closed operator algebra onto the other, and \(U\delta _e=\delta _e\).

      These are precisely the fields of Connes.FactorWitness.SpatialWitness.

      The theorem Connes.FactorWitness.tracialEquiv_of_spatialWitness restricts unitary conjugation to the two group von Neumann algebras. Connes.StarAlgEquiv.isNormal records the automatic preservation of projection suprema by the induced star-algebra equivalence and its inverse. The equation \(U\delta _e=\delta _e\) proves preservation of the canonical trace. Neither property is supplied as an extra assumption.

      For Zhou's groups, the concrete unitary composes the two Fourier models with the fiber shear. The measure-transport and von Neumann closure obligations are separated in § [connes-000D] and § [connes-000E]. Together they construct Connes.PaperFactorClosure.paperSpatialUnitary, Connes.PaperFactorClosure.paperSpatialWitness, and Connes.PaperFactorClosure.paperGroupFactors_isomorphic. This is the \(*\)-isomorphism asserted in [zhou2026icc, Proposition 3.4]; the Lean statement also records its projection-supremum preservation and preservation of the canonical trace.

      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

          Factor equivalence by Fourier shear (Zhou §3) [connes-0012]

            Spatial factor equivalence [connes-001F]
            ✍️source

              Theorem. Spatial implementation of the factor equivalence [connes-0007]
              SpatialWitnessisNormaltracialEquiv_of_spatialWitnesspaperGroupFactors_isomorphic
              L∃∀N

                The group von Neumann algebra \(L(G)\) is represented on \(\ell ^2(G)\) as the von Neumann closure of the left regular operators. Its canonical trace is the vacuum coefficient at \(\delta _e\). Consequently a unitary \(U:\ell ^2(G)\simeq \ell ^2(H)\) gives the required tracial equivalence once two facts are proved: conjugation by \(U\) carries one closed operator algebra onto the other, and \(U\delta _e=\delta _e\).

                These are precisely the fields of Connes.FactorWitness.SpatialWitness.

                The theorem Connes.FactorWitness.tracialEquiv_of_spatialWitness restricts unitary conjugation to the two group von Neumann algebras. Connes.StarAlgEquiv.isNormal records the automatic preservation of projection suprema by the induced star-algebra equivalence and its inverse. The equation \(U\delta _e=\delta _e\) proves preservation of the canonical trace. Neither property is supplied as an extra assumption.

                For Zhou's groups, the concrete unitary composes the two Fourier models with the fiber shear. The measure-transport and von Neumann closure obligations are separated in § [connes-000D] and § [connes-000E]. Together they construct Connes.PaperFactorClosure.paperSpatialUnitary, Connes.PaperFactorClosure.paperSpatialWitness, and Connes.PaperFactorClosure.paperGroupFactors_isomorphic. This is the \(*\)-isomorphism asserted in [zhou2026icc, Proposition 3.4]; the Lean statement also records its projection-supremum preservation and preservation of the canonical trace.

                Nonadditive shear and measure transport [connes-000D]
                EquivariantHaarHomeomorphpaperHaarHomeomorph
                L∃∀N

                  Proposition 3.2 proves that the fiber shear preserves Haar measure and strictly conjugates the two actions. Its quadratic correction is generally not additive, so Zhou's Remark 3.3 does not claim a compact-group automorphism. Proposition 3.4 uses only the resulting equivariant measure-space isomorphism after Fourier transform [zhou2026icc, Proposition 3.2, Remark 3.3, and Proposition 3.4].

                  The independent crossed-product discussion in [openai2026tenadvances, Chapter 4, Section 2.3, equation (2.1)] states the same abstract mechanism: group-law compatibility of the underlying compact spaces is not required.

                  The Lean boundary mirrors this distinction. The concrete Connes.PaperCrossedHaar.paperFiberShearHomeomorph and Connes.PaperCrossedHaar.paperHaarHomeomorph package continuity, measure preservation, and action equivariance, but no additive-homomorphism field.

                  At the foundation layer, Connes.CrossedProduct.EquivariantHaarHomeomorph projects this topological witness to the measurable transport interface. The extra topology is an implementation aid, not a stronger mathematical premise for the crossed-product identification.

                  A measurable equivariant isomorphism is mathematically sufficient for the abstract transport. The concrete homeomorphism is formally convenient because pullback preserves continuous coefficients. The proof uses that extra structure for the density bridge and forgets it at the measurable boundary, without falsely requiring an additive equivalence. The separate closure step is recorded in § [connes-000E].

                  Continuous coefficients and von Neumann closure [connes-000E]
                  continuousCrossedClosure_mem_iff
                  L∃∀N

                    Coordinate characters have norm-dense linear span in the continuous functions by Stone–Weierstrass. Since continuous coefficients act continuously as crossed-product multipliers, the generic continuous-coefficient closure theorem Connes.CrossedProduct.vonNeumannClosure_crossedGeneratorSetOfContinuousCoefficients_eq upgrades that density to equality of the generated von Neumann closures.

                    Pullback along the homeomorphism then gives Connes.CrossedProduct.continuousCrossedClosure_mem_iff. This does not say that continuous functions are norm-dense in \(L^\infty \); it compares the von Neumann closures generated after adjoining all continuous coefficients.

                    The paper-facing proof applies the transport and closure bridges once to each action, then composes the Fourier models with the shear. This removes parallel action-one/action-two closure plumbing while preserving Zhou's Proposition 3.4 endpoint and section order. Mapping a convenient generating family remains an intermediate step; the consumer-facing contract is equivalence of membership in the completed von Neumann algebras.