Collatz descent principle: every $n > 1$ eventually drops below $n$

Let $C$ denote the Collatz step map, $C(n)=n/2$ for even $n$ and $C(n)=3n+1$ for odd $n$. The descent principle asserts that every starting value larger than $1$ has a finite stopping time: for every $n > 1$ there exists $m \in \mathbb{N}$ with

Equivalently, no orbit started above $1$ stays at or above its starting value forever.

This is the standard reformulation of the Collatz conjecture as a well-foundedness statement. It implies the conjecture: by strong induction on $n$, the value $n=1$ reaches $1$ in zero steps, and for $n>1$ the descent principle produces a strictly smaller point $C^{m}(n)$ of the orbit, which is still positive because positivity is preserved along orbits, so the induction hypothesis applies to it and the two segments of the orbit compose. Conversely the conjecture implies the descent principle, since an orbit that reaches $1$ from $n > 1$ has passed below $n$.

The advantage of this form is that it is local: it asks only for a bounded piece of each orbit rather than for the global behaviour, and it splits cleanly along residue classes modulo $4$. The classes $n \equiv 0, 2 \pmod 4$ are settled by a single halving step and the class $n \equiv 1 \pmod 4$ with $n > 1$ by three steps, leaving $n \equiv 3 \pmod 4$ as the open case.

Formalization Note. The index $m$ is not constrained to be positive because $m = 0$ cannot witness the conclusion: $n < n$ is false.