I believe that is too strong - while we do want to consider breaking up chunks into multiple equal-feerate ones an improvement, I don’t think there is an objective reason to want the smallest ones first. (in my implementation, I do prefer smaller size when comparing equal-feerate transaction sets, but that’s an arbitrary choice that happens to prevent merging of such equal-feerate chunks).

One possibility, which I think is sufficient, is in the \gtrsim (& co) definitions is to use the total number of chunks as a tie-breaker when the fee-size diagram coincides exactly (more chunks = better). This has the advantage that “optimal linearization” automatically implies chunks which have no non-trivial subsets of the same feerate, and it doesn’t introduce a new source of incomparability. The disadvantage is that (as stated) it breaks the gathering theorem, and I suspect fixing that would complicate matters somewhat. That may also have implications for the prefix-merging algorithm’s proof (I believe the algorithm itself actually keeps its properties under this stronger ordering definition).

An alternative is leaving the preorder on linearizations alone, and instead only incorporate into the “optimal linearization” definition that chunks cannot have non-trivial subsets of higher or equal feerate. Alternatively, it could be a notion of “perfect linearization” which is stronger than optimal (and leave optimal to only be about the feerate diagram). This may be nicer in terms of presentation as the properties can be introduced and proven incrementally.