Draft: Sketch of exchanger graph_lin proof

@jaehwang.jung I'm moving incomplete proofs to MRs. Once the proofs are clear of admits they can be merged. This keeps the main development from having to maintain incomplete proofs.