I think all these steps rely really heavily on how they’re setup via the prefix intersection algorithm – eg, c_{j+1} is a chunk in \gamma_j + c_{j+1}, because \gamma_j = c_1 + c_2 + .. + c_j and c_1, c_2, .., c_n is a correct chunking, and then the fact that you generate a chunking by merging tx sets in any order means that if you add stuff on the end of that, you can start off with that chunking, and then you’ll only potentially be merging those chunks from the tail, you’ll never need to split them up.
I’m starting to have a bit of luck formalising this in lean4, fwiw, but it’s slow progress : I can convert a list of txs into a chunking, and compare fee rate graphs (evaluating the diagram at each integer byte/weight with a total fee in \mathbb Q), but currently don’t have any theorems about any of that.
(If you have a better way of defining a diagram than as a function from \mathbb N \to \mathbb Q that’d be great. I started off trying to do line segments from (s_1,f_1) \to (s_2,f_2) but that got super painful super fast)