The Cereceda (2007) conjecture holds for bipartite 2-degenerate graphs

For a graph G and a positive integer k, the k-recolouring graph Rk(G) has the proper k-colourings of G as vertices, two of them adjacent when they differ at exactly one vertex. A graph is d-degenerate if each of its non-empty subgraphs has a vertex of degree at most d. The Cereceda (2007) conjecture states that, for fixed d and k ≥ d+2, the diameter of Rk(G) is O(n²) for every d-degenerate graph G on n vertices. For d = 2, the conjecture was known to hold for k ≥ 5 by a result of Cereceda; for k = 4, the best bound known for all 2-degenerate graphs is O(n³), due to Bousquet and Heinrich. We prove that the diameter of R4(G) is at most 2n(n+1) for every bipartite 2-degenerate graph G on n vertices; hence the conjecture holds for these graphs. We also show that the order n² cannot be improved for this class, even for graphs of girth 6. For the upper bound, we fix an ordering of the vertices in which each vertex has at most two later neighbours. In n stages, we transform any proper 4-colouring into the colouring in which every vertex has the least colour not used by its later neighbours, recolouring each vertex at most twice per stage. Both of our bounds have also been proved in the Lean proof assistant.