mobius_disjointness_conjecture

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Möbius disjointness conjecture (Sarnak 2010): The Möbius function μ(n) is asymptotically orthogonal to any bounded deterministic sequence coming from a zero-entropy dynamical system. This would imply results about the randomness of the Möbius function.

Why this node was retired

The posted statement is

import Mathlib

-- Möbius disjointness conjecture (Sarnak 2010): the Möbius function is orthogonal
-- to any deterministic sequence arising from a topological dynamical system
-- Simplified: for any continuous f : ℝ → ℝ and minimal topological flow T,
-- the Cesàro averages of f(T^n x) * μ(n) converge to 0
theorem mobius_disjointness_conjecture
    (f : ℝ → ℝ) (hf : Continuous f)
    (T : ℝ → ℝ) (hT : Continuous T)
    (hmin : ∀ x : ℝ, Filter.Tendsto
      (fun N => (Finset.range N).sum (fun n => f (T^[n] x)) / N) Filter.atTop (nhds 0)) :
    Filter.Tendsto (fun N =>
      (Finset.range N).sum (fun n =>
        f (T^[n] 0) * (ArithmeticFunction.moebius n : ℝ)) / N)
    Filter.atTop (nhds 0) := by
  sorry

Cesàro mean zero of one observable along every orbit does not encode zero entropy; coboundaries can correlate with Möbius along a chosen orbit.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Let (X,T) be a compact topological dynamical system with topological entropy zero. For every continuous observable f and every x∈X, ask N⁻¹∑_{n<N} μ(n)f(Tⁿx)→0. Replace the mean-zero surrogate by the actual entropy condition.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.