EDIT: this theorem is insufficient, as it doesn’t allow for cases where the moved good transactions get chunked together with bad transactions; a scenario that is possible in the prefix-intersection merging algorithm.
Theorem
Given the following:
- A linearization L
- A topologically valid subset T of the transactions in L (which we’ll call “good” transactions).
- The good transactions merge into a single chunk of feerate f, when considered in the order they appear in in L.
- The highest chunk feerate of the bad transactions, again retaining the order of L, does not exceed f.
Under those conditions, moving the good transactions to the front of the linearization (leaving the internal order of good transactions and that of bad transactions unchanged) results in a better or equivalent linearization (by becoming the new first chunk, of feerate f).
Proof
Observe that, among the set of linearizations for the same transactions which leave the internal orderings unchanged, none can give rise to a chunk feerate exceeding f. If it did, there must be some topologically valid subset v of transactions, consisting of a union of a prefix of the good transactions and a prefix of the bad transactions, whose combined feerate exceeds f. No prefix of the bad transactions can exceed feerate f, thus there must be a prefix of the good transactions that does. This is in contradiction with the given fact that all the good transactions merge into a single chunk of feerate f.
Further observe that all good transactions merging into a single chunk of feerate f implies that any suffix of good transactions has feerate \geq f.
To prove that moving all good transactions to the front of the linearization always results in a better or equivalent linearization as the original, we will show that the following algorithm never worsens the diagram, and terminates when all the good transactions are in front:
- Compute the chunking (c_0, c_1, \ldots, c_n) of the current linearization, merging equal-feerate chunks (this does not break the monotonic decrease property, and guarantees each c_i has distinct feerate).
- Find the last chunk index t such that c_t \cap T \neq \emptyset.
- Modify the linearization by reordering the c_t transactions such that all of c_t \cap T are at the start of c_t.
- Repeat (which implies rechunking).
To show that this never worsens the diagram, it suffices to see that reordering transactions within a chunk at worst leaves the chunk unchanged, and at best splits it, which improves the diagram.
Further, this algorithm makes progress as long as c_t does not start with all its good transactions. As long as that is the case, a nonzero amount of progress towards having all the good transactions at the start of the linearization is made. Thus, after a finite number of such steps, that end state must be reached.
It remains to be shown that c_t cannot start with all its good transactions unless the end state is reached. Assume it does start with all its good transactions. The set c_t \cap T is a suffix of the good transactions, and thus has feerate \geq f. Since c_t starts with c_t \cap T, the chunk c_t itself must have feerate \geq f. However, every chunk must have feerate \leq f. The combination of those two means c_t has exactly feerate f. There can only be one such chunk (as all c_i have distinct feerates), and it must be the first one (because no higher feerate is possible), so t=0. In this case, we are in the end state, because the first chunk is the only one with good transactions, and all good transactions are at its front.