Lemma: MrTheorem18_Collatz_1c53d8a4.lift_convergence

If the Collatz orbit of n reaches 1, then the orbit of 2^r*n reaches 1 for every natural r. This propagates an established convergence result; it does not assume or prove universal convergence.

Exact formal statement

∀ (n r : Nat),
  (Exists.{1} fun k => Eq.{1} (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep k n) 1) →
    Exists.{1} fun k =>
      Eq.{1}
        (Nat.iterate.{1} Corpus.WikipediaCollatzConjecture.collatzStep k
          (HMul.hMul.{0, 0, 0} (HPow.hPow.{0, 0, 0} 2 r) n))
        1

This is a published formal lemma. Its scope is the exact statement above.

Environment availability: available.

Public JSON record