In temporal modal logic with Kripke semantics, the modal operator $\Box$ represents 'always in the future (including now)' and $\diamond$ represents 'sometimes in the future (including now)'. If we model time as a discrete, linear sequence starting at $0$ (isomorphic to $(\mathbb{N}, \le)$), which of the following modal formulas is NOT valid?