Proving that there exists an algorithm that results in an eventually consistent view of the document is trivial. However, that's not what we're talking about.

Proving that there exists an algorithm that results in an eventually consistent view of the document is trivial. However, that's not what we're talking about. Instead, researchers define a specific algorithm (e.g., involving CRDT's or OT's or something else), then prove that their algorithm results in an eventually consistent state. This reminds me a little of the relationship between proving that there exists an algorithm to factor all positive integers (this is trivial) and proving there exists a subexponential time algorithm to factor integers, which is much less trivial (see https://en.wikipedia.org/wiki/Lenstra_elliptic-curve_factorization https://en.wikipedia.org/wiki/Lenstra_elliptic-curve_factori...).