A one-vertex cut is a vertex wedge

Two finite vertex sets which cover a graph, meet in one vertex, and have no edges between their noncommon parts give a literal vertex-wedge presentation by their induced subgraphs. This is the structural extraction lemma needed to turn articulation/block data into divisor and transmission theorems.

structure Utilities.OneVertexCut (K : CFGraph) : Type u

Finite data exhibiting K as two induced pieces meeting only at glue. The no-cross condition is stated in edge-multiplicity language and therefore retains parallel edges automatically.

• left : Finset K.V

  The left vertex set of the cut, meeting the right set precisely at the glue vertex.

• right : Finset K.V

  The right vertex set of the cut; together with the left set it covers every vertex.

• glue : K.V

  The unique overlap vertex at which the two induced subgraphs are wedged.

• glue_mem_left : self.glue ∈ self.left
• glue_mem_right : self.glue ∈ self.right
• vertex_cover (z : K.V) : z ∈ self.left ∨ z ∈ self.right
• only_overlap (z : K.V) : z ∈ self.left → z ∈ self.right → z = self.glue
• no_cross (a : K.V) : a ∈ self.left → a ≠ self.glue → ∀ b ∈ self.right, b ≠ self.glue → numEdges K a b = 0

theorem Utilities.OneVertexCut.left_nonempty {K : CFGraph} (cut : OneVertexCut K) : cut.left.Nonempty

theorem Utilities.OneVertexCut.right_nonempty {K : CFGraph} (cut : OneVertexCut K) : cut.right.Nonempty

noncomputable def Utilities.OneVertexCut.leftGraph {K : CFGraph} (cut : OneVertexCut K) : CFGraph

The induced left factor.

Equations

• cut.leftGraph = Utilities.inducedSubgraph K cut.left ⋯

noncomputable def Utilities.OneVertexCut.rightGraph {K : CFGraph} (cut : OneVertexCut K) : CFGraph

The induced right factor.

Equations

• cut.rightGraph = Utilities.inducedSubgraph K cut.right ⋯

noncomputable def Utilities.OneVertexCut.leftGlue {K : CFGraph} (cut : OneVertexCut K) : cut.leftGraph.V

The common vertex as a vertex of the left induced factor.

Equations

• cut.leftGlue = ⟨cut.glue, ⋯⟩

noncomputable def Utilities.OneVertexCut.rightGlue {K : CFGraph} (cut : OneVertexCut K) : cut.rightGraph.V

The common vertex as a vertex of the right induced factor.

Equations

• cut.rightGlue = ⟨cut.glue, ⋯⟩

@[simp]

theorem Utilities.OneVertexCut.leftGlue_val {K : CFGraph} (cut : OneVertexCut K) : ↑cut.leftGlue = cut.glue

@[simp]

theorem Utilities.OneVertexCut.rightGlue_val {K : CFGraph} (cut : OneVertexCut K) : ↑cut.rightGlue = cut.glue

noncomputable def Utilities.OneVertexCut.presentation {K : CFGraph} (cut : OneVertexCut K) : VertexWedgePresentation K cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue

A one-vertex cut canonically presents the ambient graph as the wedge of its two induced factors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Utilities.OneVertexCut.graphIso {K : CFGraph} (cut : OneVertexCut K) : CFGraphIso (vertexWedge cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue) K

The occurrence-safe graph isomorphism extracted from a one-vertex cut.

Equations

• cut.graphIso = cut.presentation.graphIso

theorem Utilities.OneVertexCut.genus_eq {K : CFGraph} (cut : OneVertexCut K) : K.genus = cut.leftGraph.genus + cut.rightGraph.genus

Genus is additive across a one-vertex cut.

theorem Utilities.OneVertexCut.graph_connected_of_factors {K : CFGraph} (cut : OneVertexCut K) (hLeft : graphConnected cut.leftGraph) (hRight : graphConnected cut.rightGraph) : graphConnected K

Connected induced factors give a connected ambient graph.

theorem Utilities.OneVertexCut.BNExists_iff {K : CFGraph} (cut : OneVertexCut K) (r d : ℤ) : BNExists K r d ↔ BNExists (vertexWedge cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue) r d

Brill--Noether existence on the ambient graph is exactly existence on the extracted wedge.

theorem Utilities.OneVertexCut.BNExists_rank_one_of_factors {K : CFGraph} (cut : OneVertexCut K) (dLeft dRight : ℤ) (hLeft : BNExists cut.leftGraph 1 dLeft) (hRight : BNExists cut.rightGraph 1 dRight) : BNExists K 1 (dLeft + dRight)

Rank-one pencils on the two induced factors glue on the ambient graph, with their degrees adding.

theorem Utilities.OneVertexCut.transmissionExists_of_profile {K : CFGraph} (cut : OneVertexCut K) (u : cut.leftGraph.V) (v : cut.rightGraph.V) (tau : AspPerm) (D : CFDiv cut.leftGraph) (E : CFDiv cut.rightGraph) (hProfile : WedgeTransmissionProfile cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E u v tau) : TransmissionExists K (↑u) (↑v) tau

Arbitrary-ASP transmission profiles on the two induced factors transport to the ambient graph.

theorem Utilities.OneVertexCut.transmissionExists_sameLeft_of_profile {K : CFGraph} (cut : OneVertexCut K) (p q : cut.leftGraph.V) (tau : AspPerm) (D : CFDiv cut.leftGraph) (E : CFDiv cut.rightGraph) (hProfile : WedgeSameLeftTransmissionProfile cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E p q tau) : TransmissionExists K (↑p) (↑q) tau

An arbitrary-ASP profile with both marks on the left induced factor transports to the ambient graph.

theorem Utilities.OneVertexCut.satisfiesTransmission_map_wedgeAddDivisor_sameLeft_of_profile {K : CFGraph} (cut : OneVertexCut K) (p q : cut.leftGraph.V) (tau : AspPerm) (D : CFDiv cut.leftGraph) (E : CFDiv cut.rightGraph) (hProfile : WedgeSameLeftTransmissionProfile cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E p q tau) : SatisfiesTransmission K (↑p) (↑q) tau (cut.graphIso.mapDiv (wedgeAddDivisor cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E))

Explicit ambient witness supplied by a same-left profile across a one-vertex cut.

theorem Utilities.OneVertexCut.transmissionExists_sameRight_of_profile {K : CFGraph} (cut : OneVertexCut K) (p q : cut.rightGraph.V) (tau : AspPerm) (D : CFDiv cut.leftGraph) (E : CFDiv cut.rightGraph) (hProfile : WedgeSameRightTransmissionProfile cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E p q tau) : TransmissionExists K (↑p) (↑q) tau

An arbitrary-ASP profile with both marks on the right induced factor transports to the ambient graph.

theorem Utilities.OneVertexCut.satisfiesTransmission_map_wedgeAddDivisor_sameRight_of_profile {K : CFGraph} (cut : OneVertexCut K) (p q : cut.rightGraph.V) (tau : AspPerm) (D : CFDiv cut.leftGraph) (E : CFDiv cut.rightGraph) (hProfile : WedgeSameRightTransmissionProfile cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E p q tau) : SatisfiesTransmission K (↑p) (↑q) tau (cut.graphIso.mapDiv (wedgeAddDivisor cut.leftGraph cut.rightGraph cut.leftGlue cut.rightGlue D E))

Explicit ambient witness supplied by a same-right profile across a one-vertex cut.

Closed regression