SeedBoundary.lean

1 import PaperX.SeedConsequences
2 
3 /-!
4 The finite-graph hypothesis cannot be dropped. One isolated source plus an
5 infinite descending chain has exactly one source component but no finite cover.
6 -/
7 set_option autoImplicit false
8 namespace PaperX.SeedBoundary
9 
10 open PaperX.DirectedSeeds
11 
12 def descendingEdge (a b : Option ℕ) : Prop :=
13   ∃ n : ℕ, a = some (n+1) ∧ b = some n
14 
15 def height : Option ℕ → ℕ
16   | none => 0
17   | some n => n+1
18 
19 theorem height_injective : Function.Injective height := by
20   intro a b h
21   cases a <;> cases b <;> simp_all [height]
22 
23 theorem reach_height {a b : Option ℕ} (h : Reach descendingEdge a b) :
24     height b ≤ height a := by
25   induction h with
26   | refl => exact le_rfl
27   | @tail b c _ hbc ih =>
28     obtain ⟨n, rfl, rfl⟩ := hbc
29     simp only [height] at *
30     omega
31 
32 theorem component_singleton (a b : Option ℕ) :
33     component descendingEdge a = component descendingEdge b ↔ a = b := by
34   constructor
35   · intro h
36     obtain ⟨hab, hba⟩ := (component_eq_iff descendingEdge a b).1 h
37     exact height_injective (Nat.le_antisymm (reach_height hba) (reach_height hab))
38   · rintro rfl
39     rfl
40 
41 theorem source_exactly_none (v : Option ℕ) :
42     IsSource descendingEdge (component descendingEdge v) ↔ v = none := by
43   rw [source_iff]
44   constructor
45   · intro h
46     cases v with
47     | none => rfl
48     | some n =>
49       have hpath : Reach descendingEdge (some (n+1)) (some n) :=
50         .single ⟨n, rfl, rfl⟩
51       have hh := reach_height (h _ hpath)
52       simp only [height] at hh
53       omega
54   · rintro rfl a ha
55     rcases ha.cases_tail with h | ⟨c, _, n, _, impossible⟩
56     · subst a
57       exact .refl
58     · cases impossible
59 
60 def isolatedSource : Source descendingEdge :=
61   ⟨component descendingEdge none, (source_exactly_none none).2 rfl⟩
62 
63 theorem only_source (c : Source descendingEdge) : c = isolatedSource := by
64   have hrep := component_representative descendingEdge c.val
65   have hs : IsSource descendingEdge
66       (component descendingEdge (representative descendingEdge c.val)) := by
67     rw [hrep]
68     exact c.property
69   have hn := (source_exactly_none _).1 hs
70   apply Subtype.ext
71   change c.val = component descendingEdge none
72   rw [← hrep, hn]
73 
74 def sourceEquivUnit : Source descendingEdge ≃ Unit where
75   toFun := fun _ => ()
76   invFun := fun _ => isolatedSource
77   left_inv := fun c => (only_source c).symm
78   right_inv := fun x => by cases x; rfl
79 
80 theorem exactly_one_source : Nat.card (Source descendingEdge) = 1 := by
81   rw [Nat.card_congr sourceEquivUnit]
82   simp
83 
84 /-- There is no finite generating set, despite the unique source component. -/
85 theorem no_finite_cover (S : Finset (Option ℕ)) : ¬ Covers descendingEdge S := by
86   intro hcover
87   let N := ∑ v ∈ S, height v
88   obtain ⟨s, hs, hpath⟩ := hcover (some N)
89   have hupper : height s ≤ N := Finset.single_le_sum (fun v _ => Nat.zero_le (height v)) hs
90   have hlower := reach_height hpath
91   change N+1 ≤ height s at hlower
92   omega
93 
94 theorem no_universal_seed : ¬ ∃ s : Option ℕ, ∀ v, Reach descendingEdge s v := by
95   rintro ⟨s, hs⟩
96   exact no_finite_cover {s} (fun v => ⟨s, by simp, hs v⟩)
97 
98 end PaperX.SeedBoundary

Back to source controls