Occurrence-safe separating edges

SeparatingEdgeCut G x y records a vertex cut crossed by exactly one edge occurrence, from x on the chosen side to y outside it. The full multiplicity equation is important for multigraphs: a bridge in the underlying simple graph is not enough when parallel edge occurrences exist.

structure Utilities.SeparatingEdgeCut (G : CFGraph) (x y : G.V) : Type u

A finite cut whose unique crossing edge occurrence is x-y.

• side : Finset G.V

  The side of the cut containing x and excluding y; the validity fields require their edge to be its unique crossing occurrence.

• left_mem : x ∈ self.side
• right_not_mem : y ∉ self.side
• cross_num_edges (a b : G.V) : a ∈ self.side → b ∉ self.side → numEdges G a b = if a = x ∧ b = y then 1 else 0

theorem Utilities.SeparatingEdgeCut.endpoints_ne {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) : x ≠ y

theorem Utilities.SeparatingEdgeCut.num_edges_endpoints {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) : numEdges G x y = 1

The distinguished endpoints are joined by exactly one edge occurrence.

theorem Utilities.SeparatingEdgeCut.outdeg_eq {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) {a : G.V} (ha : a ∈ cut.side) : outdegreeSet G cut.side a = if a = x then 1 else 0

A vertex on the chosen side has one outgoing edge exactly when it is the distinguished endpoint.

theorem Utilities.SeparatingEdgeCut.intoMultiplicity_eq {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) {b : G.V} (hb : b ∉ cut.side) : Certificate.StrongSeparator.intoMultiplicity G cut.side b = if b = y then 1 else 0

A vertex outside the chosen side has one incoming edge exactly when it is the distinguished endpoint.

theorem Utilities.SeparatingEdgeCut.prin_indicator_script {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) : (prin G) (indicatorScript G cut.side) = oneChip y - oneChip x

Firing the chosen side transfers one chip across its unique separating edge.

theorem Utilities.SeparatingEdgeCut.chipEquivalent {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) : linearEquiv G (oneChip x) (oneChip y)

The endpoints of a separating edge represent the same degree-one divisor class.

Normalizing a firing script across one separating edge

def Utilities.SeparatingEdgeCut.normalizeScript {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : firingScript G

Add a constant on the chosen side so that the firing levels at the two bridge endpoints agree.

Equations

• cut.normalizeScript sigma = sigma + (sigma y - sigma x) • indicatorScript G cut.side

@[simp]

theorem Utilities.SeparatingEdgeCut.normalizeScript_left {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : cut.normalizeScript sigma x = sigma y

@[simp]

theorem Utilities.SeparatingEdgeCut.normalizeScript_right {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : cut.normalizeScript sigma y = sigma y

theorem Utilities.SeparatingEdgeCut.normalizeScript_endpoints_eq {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : cut.normalizeScript sigma x = cut.normalizeScript sigma y

Normalization really equalizes the two endpoint levels.

theorem Utilities.SeparatingEdgeCut.prin_normalizeScript {G : CFGraph} {x y : G.V} (cut : SeparatingEdgeCut G x y) (sigma : firingScript G) : (prin G) (cut.normalizeScript sigma) = (prin G) sigma + (sigma y - sigma x) • (oneChip y - oneChip x)

The exact change in the principal divisor under one bridge normalization.

theorem Utilities.SeparatingEdgeCut.endpoints_same_side_or_same_edge {G : CFGraph} {x y a b : G.V} (cut : SeparatingEdgeCut G x y) (other : SeparatingEdgeCut G a b) : (a ∈ cut.side ↔ b ∈ cut.side) ∨ a = x ∧ b = y ∨ a = y ∧ b = x

Two separating edges cannot cross one another. Relative to the chosen side of cut, the endpoints of other lie on the same side unless other is the very same unoriented bridge occurrence.

theorem Utilities.SeparatingEdgeCut.normalizeScript_preserves_endpoints_eq {G : CFGraph} {x y a b : G.V} (cut : SeparatingEdgeCut G x y) (other : SeparatingEdgeCut G a b) (sigma : firingScript G) (hEqual : sigma a = sigma b) : cut.normalizeScript sigma a = cut.normalizeScript sigma b

Normalizing across one separating edge preserves equality across every other separating edge that was already normalized.