Transporting a local Dhar move out of an induced subgraph

A configuration picture is a firing script together with a proof that the residual it leaves is effective. Every picture in the library is written on the whole graph, and that is why the library has no picture for a component whose shape is understood but whose ambient graph is large: the arithmetic has to be redone in the ambient graph.

This file removes that obstacle. Fix a vertex set A. Call a vertex Interior G A when every ambient edge at it stays inside A; the vertices of A that are not interior are its boundary. The observation is:

A firing script whose support consists of interior vertices acts on the ambient graph exactly as its restriction acts on the induced subgraph G[A], and does nothing at all outside A.

Hence a local Dhar move performed inside G[A] -- subject only to the side condition that the script vanish on the boundary of A -- proves the ambient reachability statement, provided the ambient divisor is effective off A. reaches_of_induced_script is that theorem.

Why this is the gluing lemma

When A has a single boundary vertex g, the side condition costs nothing: firing scripts matter only up to a constant, so any script may be normalised to vanish at g. That special case is exactly the vertex-wedge delivery statement (Utilities.OneVertexCut, winnable_vertexWedge_iff_exists_chipShift), and reaches_of_induced_script_of_unique_boundary states it in this language.

The general form is strictly stronger, and the strength is what pictures need: A may have any number of boundary vertices, so the ambient graph need not have a cut vertex at all. A chip-free component sitting inside a two-edge-connected ambient graph still localises, at the price of the boundary vertices being frozen -- which, read as a divisor statement, says that a boundary vertex may deliver into A only the chips it already carries.

Layering

Utilities only, so every LowGenus configuration file may use it.

Interior vertices

def Utilities.Gluing.Interior (G : CFGraph) (A : Finset G.V) (v : G.V) : Prop

v is interior to A when every ambient edge at v has its other end in A. A script supported on interior vertices cannot be felt outside A.

Equations

• Utilities.Gluing.Interior G A v = ∀ w ∉ A, numEdges G v w = 0

theorem Utilities.Gluing.num_edges_eq_zero_of_interior {G : CFGraph} {A : Finset G.V} {u w : G.V} (hu : Interior G A u) (hw : w ∉ A) : numEdges G w u = 0

An interior vertex is invisible from outside A.

Extending a script from the induced subgraph

noncomputable def Utilities.Gluing.extendScript (G : CFGraph) (A : Finset G.V) (hA : A.Nonempty) (t : firingScript (inducedSubgraph G A hA)) : firingScript G

Extend a script on G[A] by zero.

Equations

• Utilities.Gluing.extendScript G A hA t v = if h : v ∈ A then t ⟨v, h⟩ else 0

@[simp]

theorem Utilities.Gluing.extendScript_of_mem {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} (t : firingScript (inducedSubgraph G A hA)) {v : G.V} (hv : v ∈ A) : extendScript G A hA t v = t ⟨v, hv⟩

@[simp]

theorem Utilities.Gluing.extendScript_of_not_mem {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} (t : firingScript (inducedSubgraph G A hA)) {v : G.V} (hv : v ∉ A) : extendScript G A hA t v = 0

def Utilities.Gluing.SupportInterior {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} (t : firingScript (inducedSubgraph G A hA)) : Prop

The script's support consists of interior vertices.

Equations

• Utilities.Gluing.SupportInterior t = ∀ (x : (Utilities.inducedSubgraph G A hA).V), t x ≠ 0 → Utilities.Gluing.Interior G A ↑x

theorem Utilities.Gluing.supportInterior_of_vanishing_on_boundary {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} {t : firingScript (inducedSubgraph G A hA)} (B : Finset G.V) (hB : ∀ (x : (inducedSubgraph G A hA).V), ↑x ∉ B → Interior G A ↑x) (hVanish : ∀ (x : (inducedSubgraph G A hA).V), ↑x ∈ B → t x = 0) : SupportInterior t

The practical form of the side condition: name a finite set B containing every non-interior vertex of A, and check that the script vanishes on it.

The transport computation

theorem Utilities.Gluing.prin_extendScript_of_not_mem {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} {t : firingScript (inducedSubgraph G A hA)} (ht : SupportInterior t) {v : G.V} (hv : v ∉ A) : (prin G) (extendScript G A hA t) v = 0

Outside A the extended script does nothing.

theorem Utilities.Gluing.prin_extendScript_of_mem {G : CFGraph} {A : Finset G.V} {hA : A.Nonempty} {t : firingScript (inducedSubgraph G A hA)} (ht : SupportInterior t) {v : G.V} (hv : v ∈ A) : (prin G) (extendScript G A hA t) v = (prin (inducedSubgraph G A hA)) t ⟨v, hv⟩

Inside A the extended script acts exactly as it does on G[A].

The transport theorem

theorem Utilities.Gluing.reaches_of_induced_script {G : CFGraph} {A : Finset G.V} (hA : A.Nonempty) {D : CFDiv G} (hOff : ∀ v ∉ A, 0 ≤ D v) {p : G.V} (hp : p ∈ A) {t : firingScript (inducedSubgraph G A hA)} (ht : SupportInterior t) (hEff : effective ((fun (x : (inducedSubgraph G A hA).V) => D ↑x) - oneChip ⟨p, hp⟩ + (prin (inducedSubgraph G A hA)) t)) : Certificate.StrongSeparator.Reaches G D p

A local Dhar move inside G[A] proves ambient reachability.

The hypotheses are exactly three:

• the ambient divisor is effective away from A (nothing outside is spent);
• the target lies in A;
• the script is supported on interior vertices -- equivalently, it vanishes on the boundary of A.

Under them, an effective residual computed entirely inside the induced subgraph G[A] is an effective ambient residual.

The one-boundary case: a vertex gluing, where the side condition is free

theorem Utilities.Gluing.reaches_of_induced_script_of_unique_boundary {G : CFGraph} {A : Finset G.V} (hA : A.Nonempty) {g : G.V} (hg : g ∈ A) (hBoundary : ∀ u ∈ A, u ≠ g → Interior G A u) {D : CFDiv G} (hOff : ∀ v ∉ A, 0 ≤ D v) {p : G.V} (hp : p ∈ A) (t : firingScript (inducedSubgraph G A hA)) (hEff : effective ((fun (x : (inducedSubgraph G A hA).V) => D ↑x) - oneChip ⟨p, hp⟩ + (prin (inducedSubgraph G A hA)) t)) : Certificate.StrongSeparator.Reaches G D p

The vertex-gluing case. If g is the only vertex of A with an edge leaving A, the interior side condition is free: normalise the script to vanish at g. This is the delivery statement for a one-vertex cut, and it needs no hypothesis on the script at all.