Rooted tree copies supported on word prefixes

attachLeaves S r s adds s new pendant vertices at the vertex r of S, and a copy of S in a host graph extends to a copy of attachLeaves S r 1 whenever some neighbour of the image of r is unused (attach_single_leaf_copy).

RootedWordFamily S r G b X says that S has a copy in G sending the root r to b and every other vertex into X; rootedWordCount S r G l₀ counts the cut permutation words of l₀ supporting such a copy on their prefix. Moving the root to a newly attached leaf costs at most one word per permutation (rooted_word_leaf_move_count), and two rooted trees glued at a common root satisfy the branch gluing inequality (rooted_word_branch_gluing_count).

Deleting the edge rs of a tree leaves two trees (tree_edge_partition), so a root of degree at least two splits a finite tree into two strictly smaller rooted trees meeting only at the root (tree_root_partition), and removing a leaf and re-attaching it is an isomorphism (leafRestoreIso). A strong induction on the order t of the tree then proves rooted_word_tree_bound: the adjacency-marked cut permutation words of a repetition-free host word l₀ number at most those supporting a rooted copy of the tree plus (t - 2) · |l₀|!.

Attaching leaves to a graph.

def Erdos548.attachLeaves {V : Type u_1} (S : SimpleGraph V) (r : V) (s : ℕ) : SimpleGraph (V ⊕ Fin s)

Attach a set of new leaves to a fixed vertex.

Equations

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

theorem Erdos548.attach_single_leaf_copy {U : Type u_1} {V : Type u_2} (S : SimpleGraph U) (G : SimpleGraph V) (r : U) (f : S.Copy G) (w : V) (hw : G.Adj (f r) w) (hfree : w ∉ Set.range ⇑f) : ∃ (F : (attachLeaves S r 1).Copy G), (∀ (x : U), F (Sum.inl x) = f x) ∧ F (Sum.inr 0) = w

Rooted graph copies in permutation-word prefixes and the leaf-root move.

def Erdos548.RootedWordFamily {U : Type u_1} {V : Type u_2} [DecidableEq V] (S : SimpleGraph U) (r : U) (G : SimpleGraph V) (b : V) (X : Finset V) : Prop

A rooted copy supported on the root image and the displayed outer set.

Equations

• Erdos548.RootedWordFamily S r G b X = ∃ (f : S.Copy G), f r = b ∧ ∀ (x : U), f x ∈ insert b X

noncomputable def Erdos548.rootedWordCount {U : Type u_1} {V : Type u_2} [DecidableEq V] (S : SimpleGraph U) (r : U) (G : SimpleGraph V) (l₀ : List V) : ℕ

The number of cut permutation words of l₀ supporting a rooted copy of S with root at the first letter.

Equations

• Erdos548.rootedWordCount S r G l₀ = Erdos548.fullWordCount l₀ G.Adj (Erdos548.RootedWordFamily S r G)

theorem Erdos548.rootedWordFamily_mono {U : Type u_1} {V : Type u_2} [DecidableEq V] (S : SimpleGraph U) (r : U) (G : SimpleGraph V) (b : V) {X Y : Finset V} (hXY : X ⊆ Y) : RootedWordFamily S r G b X → RootedWordFamily S r G b Y

theorem Erdos548.rooted_word_leaf_move_step {U : Type u_1} {V : Type u_2} [DecidableEq V] (S : SimpleGraph U) (r : U) (G : SimpleGraph V) (l : List V) (hl : l.Nodup) (k : ℕ) (hk : k < l.length) (hs : FullWordQualifies G.Adj (RootedWordFamily S r G) l k) (j : ℕ) (hjk : j < k) (hj : FullWordQualifies G.Adj (RootedWordFamily S r G) l j) : FullWordQualifies G.Adj (RootedWordFamily (attachLeaves S r 1) (Sum.inr 0) G) (reverseWordAt l (k + 1)) k

theorem Erdos548.rooted_word_leaf_move_count {U : Type u_1} {V : Type u_2} [DecidableEq V] (S : SimpleGraph U) (r : U) (G : SimpleGraph V) (l₀ : List V) (hl : l₀.Nodup) : rootedWordCount S r G l₀ ≤ rootedWordCount (attachLeaves S r 1) (Sum.inr 0) G l₀ + (permutationWords l₀).card

theorem Erdos548.rootedWordFamily_iso_iff {U : Type u_1} {W : Type u_2} {V : Type u_3} [DecidableEq V] {S : SimpleGraph U} {T : SimpleGraph W} (e : S ≃g T) (r : U) (G : SimpleGraph V) (b : V) (X : Finset V) : RootedWordFamily T (e r) G b X ↔ RootedWordFamily S r G b X

theorem Erdos548.rootedWordCount_iso {U : Type u_1} {W : Type u_2} {V : Type u_3} [DecidableEq V] {S : SimpleGraph U} {T : SimpleGraph W} (e : S ≃g T) (r : U) (G : SimpleGraph V) (l₀ : List V) : rootedWordCount T (e r) G l₀ = rootedWordCount S r G l₀

theorem Erdos548.rootedWordFamily_restrict {U : Type u_1} {V : Type u_2} [DecidableEq V] (T : SimpleGraph U) (G : SimpleGraph V) (A : Set U) (r : U) (hr : r ∈ A) (b : V) (X : Finset V) : RootedWordFamily T r G b X → RootedWordFamily (SimpleGraph.induce A T) ⟨r, hr⟩ G b X

theorem Erdos548.rootedWordFamily_glue {U : Type u_1} {V : Type u_2} [DecidableEq V] (T : SimpleGraph U) (G : SimpleGraph V) (A : Set U) (r : U) (hr : r ∈ A) (hsep : ∀ x ∈ A, ∀ y ∉ A, T.Adj x y → x = r) (b : V) (R X : Finset V) (hd : Disjoint R X) (hf : RootedWordFamily (SimpleGraph.induce A T) ⟨r, hr⟩ G b R) (hg : RootedWordFamily (SimpleGraph.induce (Aᶜ ∪ {r}) T) ⟨r, ⋯⟩ G b X) : RootedWordFamily T r G b (R ∪ X)

Two copies agree at the root. Disjoint outer supporting sets ensure that no other images collide.

theorem Erdos548.rooted_word_branch_gluing_count {U : Type u_1} {V : Type u_2} [DecidableEq V] (T : SimpleGraph U) (G : SimpleGraph V) (A : Set U) (r : U) (hr : r ∈ A) (hsep : ∀ x ∈ A, ∀ y ∉ A, T.Adj x y → x = r) (l₀ : List V) (hl : l₀.Nodup) (hne : l₀ ≠ []) : rootedWordCount (SimpleGraph.induce A T) ⟨r, hr⟩ G l₀ + rootedWordCount (SimpleGraph.induce (Aᶜ ∪ {r}) T) ⟨r, ⋯⟩ G l₀ ≤ (fullWordCount l₀ G.Adj fun (x : V) (x_1 : Finset V) => True) + (permutationWords l₀).card + rootedWordCount T r G l₀

Splitting finite trees at an edge or at a root.

theorem Erdos548.tree_edge_partition {U : Type} (T : SimpleGraph U) (hT : T.IsTree) (r s : U) (hrs : T.Adj r s) : ∃ (A : Set U), r ∈ A ∧ s ∉ A ∧ (SimpleGraph.induce A T).IsTree ∧ (SimpleGraph.induce Aᶜ T).IsTree ∧ ∀ x ∈ A, ∀ y ∉ A, T.Adj x y → x = r ∧ y = s

theorem Erdos548.tree_root_partition {U : Type} [Finite U] (T : SimpleGraph U) (hT : T.IsTree) (r s z : U) (hrs : T.Adj r s) (hrz : T.Adj r z) (hsz : s ≠ z) : ∃ (A : Set U) (_ : r ∈ A), (SimpleGraph.induce A T).IsTree ∧ (SimpleGraph.induce (Aᶜ ∪ {r}) T).IsTree ∧ 2 ≤ Nat.card ↑A ∧ 2 ≤ Nat.card ↑(Aᶜ ∪ {r}) ∧ Nat.card ↑A < Nat.card U ∧ Nat.card ↑(Aᶜ ∪ {r}) < Nat.card U ∧ Nat.card ↑A + Nat.card ↑(Aᶜ ∪ {r}) = Nat.card U + 1 ∧ ∀ x ∈ A, ∀ y ∉ A, T.Adj x y → x = r

noncomputable def Erdos548.leafRestoreIso {U : Type} (T : SimpleGraph U) (l p : U) (hlp : T.Adj l p) (honly : ∀ (x : U), T.Adj l x → x = p) : attachLeaves (SimpleGraph.induce {l}ᶜ T) ⟨p, ⋯⟩ 1 ≃g T

Removing a leaf l with unique neighbour p and attaching one new leaf at p gives back the original graph, up to isomorphism.

Equations

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

@[simp]

theorem Erdos548.leafRestoreIso_inl {U : Type} (T : SimpleGraph U) (l p : U) (hlp : T.Adj l p) (honly : ∀ (x : U), T.Adj l x → x = p) (x : ↑{l}ᶜ) : (leafRestoreIso T l p hlp honly) (Sum.inl x) = ↑x

@[simp]

theorem Erdos548.leafRestoreIso_inr {U : Type} (T : SimpleGraph U) (l p : U) (hlp : T.Adj l p) (honly : ∀ (x : U), T.Adj l x → x = p) : (leafRestoreIso T l p hlp honly) (Sum.inr 0) = l

The rooted word-count bound for every finite tree.

theorem Erdos548.rootedWordFamily_of_card_two {U : Type u_1} {V : Type u_2} [Fintype U] [DecidableEq V] (T : SimpleGraph U) (r : U) (ht : Fintype.card U = 2) (G : SimpleGraph V) (b w : V) (hbw : G.Adj b w) (X : Finset V) (hw : w ∈ X) : RootedWordFamily T r G b X

theorem Erdos548.rooted_word_count_base {U : Type u_1} {V : Type u_2} [Fintype U] [DecidableEq V] (T : SimpleGraph U) (r : U) (ht : Fintype.card U = 2) (G : SimpleGraph V) (l₀ : List V) : (fullWordCount l₀ G.Adj fun (x : V) (x_1 : Finset V) => True) ≤ rootedWordCount T r G l₀

theorem Erdos548.rooted_word_tree_bound_aux (t : ℕ) (U V : Type) [Fintype U] [DecidableEq V] (T : SimpleGraph U) (r : U) (_hT : T.IsTree) (_ht : Fintype.card U = t) (_ht2 : 2 ≤ t) (G : SimpleGraph V) (l₀ : List V) (_hl : l₀.Nodup) (_hne : l₀ ≠ []) : (fullWordCount l₀ G.Adj fun (x : V) (x_1 : Finset V) => True) ≤ rootedWordCount T r G l₀ + (t - 2) * (permutationWords l₀).card

theorem Erdos548.rooted_word_tree_bound {U V : Type} [Fintype U] [DecidableEq V] (T : SimpleGraph U) (r : U) (hT : T.IsTree) (ht2 : 2 ≤ Fintype.card U) (G : SimpleGraph V) (l₀ : List V) (hl : l₀.Nodup) (hne : l₀ ≠ []) : (fullWordCount l₀ G.Adj fun (x : V) (x_1 : Finset V) => True) ≤ rootedWordCount T r G l₀ + (Fintype.card U - 2) * (permutationWords l₀).card