A one-vertex cut is the free case of the transport lemma

Utilities.Gluing.reaches_of_induced_script localizes a picture to an induced subgraph at the price of freezing the script on the boundary. This file records that a OneVertexCut is exactly the case where that price is zero: the cut's no_cross field says the glue vertex is the only vertex of left with an edge leaving left, and a script may always be normalised to vanish at one prescribed vertex.

So the transport lemma subsumes the vertex-wedge delivery statement, and this file is the machine-checked form of that claim. What the transport lemma adds beyond it is the case of a larger boundary, which a OneVertexCut cannot express and which is what a chip-free component of a two-edge-connected core actually presents.

theorem Utilities.Gluing.interior_left_of_oneVertexCut {K : CFGraph} (cut : OneVertexCut K) {u : K.V} (hu : u ∈ cut.left) (hne : u ≠ cut.glue) : Interior K cut.left u

Away from the glue vertex, every vertex of the left half of a one-vertex cut is interior to it.

theorem Utilities.Gluing.reaches_of_oneVertexCut_left {K : CFGraph} (cut : OneVertexCut K) {D : CFDiv K} (hOff : ∀ v ∉ cut.left, 0 ≤ D v) {p : K.V} (hp : p ∈ cut.left) (t : firingScript cut.leftGraph) (hEff : effective ((fun (x : cut.leftGraph.V) => D ↑x) - oneChip ⟨p, hp⟩ + (prin cut.leftGraph) t)) : Certificate.StrongSeparator.Reaches K D p

A picture proved on the left factor of a one-vertex cut is a picture on the ambient graph. No condition on the script: a one-vertex cut is the free case of reaches_of_induced_script.