SeedConsequences.lean

1 import PaperX.DirectedSeeds
2 import Mathlib.Tactic
3 
4 /-! Consequences of actual directed reachability; no arithmetic transport is postulated. -/
5 set_option autoImplicit false
6 namespace PaperX.SeedConsequences
7 
8 open PaperX.DirectedSeeds
9 universe u
10 variable {V : Type u} (E : V → V → Prop)
11 
12 /-- Any choice of one representative of each source component is optimal. -/
13 theorem arbitrary_representatives [Finite V] (s : Source E → V)
14     (hs : ∀ c, component E (s c) = c.val) :
15     ∃ S : Finset V, (∀ v, v ∈ S ↔ ∃ c, s c = v) ∧ Covers E S ∧
16       S.card = seedRank E := by
17   classical
18   let S := Finset.univ.image s
19   have hinj : Function.Injective s := by
20     intro a b hab
21     apply Subtype.ext
22     exact (hs a).symm.trans ((congrArg (component E) hab).trans (hs b))
23   refine ⟨S, ?_, ?_, ?_⟩
24   · intro v
25     simp [S]
26   · apply (covers_iff_meets_sources E S).2
27     intro c
28     exact ⟨s c, Finset.mem_image.mpr ⟨c, Finset.mem_univ c, rfl⟩, hs c⟩
29   · rw [directed_minimum_seed]
30     simp [S, Finset.card_image_of_injective _ hinj, Nat.card_eq_fintype_card]
31 
32 /-- No new admissible edges can increase the minimum number of seeds. -/
33 theorem seedRank_antitone [Finite V] (F : V → V → Prop)
34     (hEF : ∀ a b, E a b → F a b) : seedRank F ≤ seedRank E := by
35   obtain ⟨S, hS, hcard⟩ := seedRank_realized E
36   rw [← hcard]
37   apply seedRank_le F S
38   intro v
39   obtain ⟨s, hs, hsv⟩ := hS v
40   exact ⟨s, hs, Relation.ReflTransGen.mono hEF s v hsv⟩
41 
42 /-- Directed transport preserves a supplied property only when every edge does. -/
43 theorem transfer_along_path (P : V → Prop)
44     (hP : ∀ a b, E a b → P a → P b) {a b : V} (h : Reach E a b) :
45     P a → P b := by
46   induction h with
47   | refl => exact id
48   | @tail b c _ hbc ih => exact fun ha => hP b c hbc (ih ha)
49 
50 theorem transfer_from_seeds (P : V → Prop)
51     (hP : ∀ a b, E a b → P a → P b) (S : Finset V)
52     (hcover : Covers E S) (hseed : ∀ s ∈ S, P s) : ∀ v, P v := by
53   intro v
54   obtain ⟨s, hs, hsv⟩ := hcover v
55   exact transfer_along_path E P hP hsv (hseed s hs)
56 
57 /-- A finite graph has rank zero precisely when it has no vertices. -/
58 theorem rank_zero_iff [Finite V] : seedRank E = 0 ↔ IsEmpty V := by
59   classical
60   constructor
61   · intro h
62     obtain ⟨S, hS, hc⟩ := seedRank_realized E
63     have hnil : S = ∅ := Finset.card_eq_zero.mp (hc.trans h)
64     refine ⟨fun v => ?_⟩
65     obtain ⟨s, hs, _⟩ := hS v
66     simp [hnil] at hs
67   · intro h
68     let : IsEmpty V := h
69     apply Nat.eq_zero_of_le_zero
70     simpa using seedRank_le E ∅ (fun v => isEmptyElim v)
71 
72 /-- One universal seed exists exactly when the independently minimized rank is one. -/
73 theorem rank_one_iff [Finite V] :
74     seedRank E = 1 ↔ ∃ s : V, ∀ v, Reach E s v := by
75   classical
76   constructor
77   · intro h
78     obtain ⟨S, hS, hc⟩ := seedRank_realized E
79     obtain ⟨s, rfl⟩ := Finset.card_eq_one.mp (hc.trans h)
80     refine ⟨s, fun v => ?_⟩
81     obtain ⟨t, ht, htv⟩ := hS v
82     have hts : t = s := Finset.mem_singleton.mp ht
83     exact hts ▸ htv
84   · rintro ⟨s, hs⟩
85     have hupper : seedRank E ≤ 1 := by
86       simpa using seedRank_le E {s} (fun v => ⟨s, by simp, hs v⟩)
87     have hnonzero : seedRank E ≠ 0 := by
88       intro hzero
89       exact ((rank_zero_iff E).1 hzero).false s
90     omega
91 
92 theorem one_source_iff_universal_seed [Finite V] :
93     Nat.card (Source E) = 1 ↔ ∃ s : V, ∀ v, Reach E s v := by
94   rw [← directed_minimum_seed, rank_one_iff]
95 
96 end PaperX.SeedConsequences

Back to source controls