And let's not forget that the official paper on Yjs is just plain wrong, the "proofs" it contains are circular. They look nice, but they are wrong.
Could you elaborate on that or share a source? It sounds like it'd be not just interesting but important to learn.
This was my impression as well. If you ignore the paper and just look at the source code - and carefully study Seph Gentle's Yjs-like RGA implementation [1] - I believe you find that it is equivalent to an RGA-style tree, but with a different rule for sorting insertions having the same left origin. That rule is hard to describe but can eventually be proved commutative; I'm hoping to include this in a paper someday.
[1] https://josephg.com/blog/crdts-are-the-future/