I'm interested in making a little list of papers that include a proof that lattice surgery really does what it claims to do; namely, performs a pairwise logical measurement. The original paper (http://arxiv.org/abs/1111.4022) gives a detailed sketch of what the protocol does but perhaps doesn't quite constitute a rigorous proof that it really works. A couple of papers (http://arxiv.org/abs/1810.10037, http://arxiv.org/abs/1704.08670) prove that the merge step of the protocol is a projector at the logical level, and the splitting step is its adjoint. A third uses low-level ZX-calculus (http://arxiv.org/abs/2204.14038), and a fourth uses the stabilizer formalism (http://arxiv.org/abs/2006.03071).
Are there other papers out there you know of that contain a proof that lattice surgery works as described? Only needs to be for a specific example code (e.g. surface code of a certain size). Thanks in advance!