sarnak_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.

Sarnak's Conjecture: The Möbius function $\mu(n)$ is asymptotically orthogonal to any sequence arising from a zero-topological-entropy dynamical system. For any compact metric space $(X, d)$, continuous $T: X \to X$ of zero topological entropy, continuous $f: X \to \mathbb{R}$, and $x \in X$:

Proposed by Sarnak (2009). Implies Chowla's conjecture. Known for many specific systems (horocycle flows, nilsequences, Thue-Morse, Pascal's triangle mod 2, etc.) but the general case remains open.

Source: Sarnak, P. (2011). Three Lectures on the Möbius Function. IAS Letter. DOI:10.4169/mathhorizons191.04

Why this node was retired

The posted statement is

theorem sarnak_conjecture (α : Type*) [MetricSpace α] [CompactSpace α]
    (T : α → α) (hT : Continuous T)
    (hzero_entropy : ∀ ε : ℝ, 0 < ε → ∃ s : Finset α,
      ∀ x : α, ∃ y ∈ s, dist x y < ε)
    (f : ContinuousMap α ℝ) (x : α) :
    Filter.Tendsto (fun N : ℕ =>
      (1 : ℝ) / N * ∑ n ∈ Finset.range N,
        (ArithmeticFunction.moebius (n + 1) : ℝ) * f (T^[n] x))
      Filter.atTop (nhds 0) := by
  sorry

The supposed zero-entropy hypothesis is only existence of finite ε-nets, already automatic on compact metric spaces and independent of T.

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

Proposed corrected statement

Define topological entropy through separated/spanning orbit sets or open covers and require h_top(T)=0. Retain compactness, continuity and the universal Möbius-disjointness conclusion.

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.