Merging incomparable linearizations

Implementation
,
16

(I’m finding it hard to work out a decent way of comparing diagrams that doesn’t get lost in details really quickly. Perhaps the problem is that I really only want to compare orderings of a given set of transactions after chunking them, not compare two orderings of potentially two different sets of transactions with arbitrary groupings)

Anyway, I guess the general case I’m going for here is

\epsilon_n + \delta_j \ge \gamma_j + \zeta_j

Those are comprised of the exact same txs, ie d_1, .., d_j and e_1, .., e_n, but in different orders. The QED step is setting j=n giving \zeta_j=\emptyset, and thus R_1 + (L_2 - R_1) = \epsilon_n + \delta_n \ge \gamma_n = L_2. \ge is a diagram comparison after chunking the txs, and +, \sum are concatenation.

The initial step for j=0 is easy: \delta_0 = \gamma_0 = \emptyset and \epsilon_n = \zeta_0 by construction.

The inductive step is to show \epsilon_n + \delta_{j+1} \ge \gamma_{j+1} + \zeta_{j+1}. To show that, we have:

\begin{align} \epsilon_n + \delta_{j+1} &= (\epsilon_n + \delta_j) + d_{j+1} \\ &\ge (\gamma_j + \zeta_j) + d_{j+1} \\ &= \gamma_j + (e_{j+1} + \zeta_{j+1}) + d_{j+1} \\ &\ge \gamma_j + e_{j+1} + (d_{j+1}) + \zeta_{j+1} \\ &\ge \gamma_j + (c_{j+1}) + \zeta_{j+1} \\ &= \gamma_{j+1} + \zeta_{j+1} \end{align}

Note that this chain is from best linearisation to worse. Steps are:

  • inductive hypothesis
  • moving d_{j+1} after \zeta_{j+1} improves things (observe that \zeta_{j+1} has a higher feerate than any chunk)
  • reordering the chunk c_{j+1} into e_{j+1} + d_{j+1} doesn’t make things worse

Not sure how to properly formalise those steps yet, but I think they’re okay.