for reference, the statement has been formalized in Lean in Deepmind's open problem database: https://github.com/google-deepmind/formal-conjectures/blob/e...