@[reducible, inline]

abbrev after {n : ℕ} (σ : List (Call n)) : GossipState n

Equations

• after σ = makeCalls (initialState n) σ

Helper functions about properties of Nats.

theorem exists_to_minimal_exists (φ : ℕ → Prop) : (∃ (k : ℕ), φ k) → ∃ (m : ℕ), φ m ∧ ∀ n < m, ¬φ n

Suppose there exists a natural number satisfying φ. Then there exists a minimal natural number that satisfies φ.

def noHo {n : ℕ} (σ : List (Call n)) : Prop

Nobody hears their own secret in the given sequence, i.e. before each call in the sequence, the agents in that call do not know each other's secrets.

Equations

• noHo σ = ∀ (i : Fin σ.length), ¬after (List.take (↑i - 1) σ) σ[i].1 σ[i].2 ∧ ¬after (List.take (↑i - 1) σ) σ[i].2 σ[i].1

def v {m : ℕ} (S : List (Call m)) (k : Fin m) : ℕ

Number of calls that k directly participates in.

Equations

• v S k = List.countP (fun (c : Call m) => decide (c.1 = k ∨ c.2 = k)) S

theorem exp_needs_n_min_one_calls {n : ℕ} {k : Fin n} (S : List (Call n)) (h : isExpert (after S) k) : n - 1 < S.length

Among n agents, to make k an expert, we need at least n-1 calls.

theorem known_needs_n_min_one_calls {n : ℕ} {k : Fin n} (S : List (Call n)) (h : allKnow (after S) k) : n - 1 < S.length

Among n agents, to make everyone know k's secret, we need at least n-1 calls.

theorem noHo_exp_and_known_needs_many_calls {n : ℕ} (S : List (Call n)) (S_noHo : noHo S) (k : Fin n) (h : isExpert (after S) k) (h2 : allKnow (after S) k) : 2 * n - 2 - v S k ≤ S.length

Given a noHo sequence, to make k an expert and make everyone know k, we need this many calls.

def is_f (n k : ℕ) : Prop

f(n) = k

Equations

• is_f n k = ∃ (σ : List (Call n)), allExpert (after σ) ∧ σ.length = k ∧ ¬∃ (σ' : List (Call n)), allExpert (after σ') ∧ σ'.length < k

def is_f_leq (n k : ℕ) : Prop

Equations

• is_f_leq n k = ∃ (σ : List (Call n)), allExpert (after σ) ∧ σ.length ≤ k

def phi (n : ℕ) : Prop

Equations

• phi n = (n > 4 ∧ is_f_leq n (2 * n - 5))

def is_minimal (m : ℕ) : Prop

Equations

• is_minimal m = (phi m ∧ ∀ n < m, ¬phi n)

def initial {m : ℕ} (S : List (Call m)) (k : Fin m) : Option (Call m)

Equations

• initial S k = List.find? (fun (c : Call m) => decide (c.1 = k ∨ c.2 = k)) S

def final {m : ℕ} (S : List (Call m)) (k : Fin m) : Option (Call m)

Equations

• final S k = List.find? (fun (c : Call m) => decide (c.1 = k ∨ c.2 = k)) S.reverse

def isAgentInitialCall {m : ℕ} (S : List (Call m)) (k : Fin m) (c : Call m) : Bool

Equations

• isAgentInitialCall S k c = decide (initial S k = some c)

def isAgentFinalCall {m : ℕ} (S : List (Call m)) (k : Fin m) (c : Call m) : Bool

Equations

• isAgentFinalCall S k c = decide (final S k = some c)

def isInitialCall {m : ℕ} (S : List (Call m)) (c : Call m) : Bool

Equations

• isInitialCall S c = decide (isAgentInitialCall S c.1 c = true ∨ isAgentInitialCall S c.2 c = true)

def isFinalCall {m : ℕ} (S : List (Call m)) (c : Call m) : Bool

Equations

• isFinalCall S c = decide (isAgentFinalCall S c.1 c = true ∨ isAgentFinalCall S c.2 c = true)

theorem noHo_of_minimal_expert_sequence {m : ℕ} (σ : List (Call m)) (σ_short : σ.length ≤ 2 * m - 5) (hExp : allExpert (after σ)) (h_min : is_minimal m) : noHo σ

Given a sequence σ of length 2m-5 or less that makes all m agents experts, if m is minimal, then nobody hears their own secret in σ.

theorem initial_both_or_neither {m : ℕ} (S : List (Call m)) (c : Call m) : c ∈ S → isAgentInitialCall S c.1 c = true ∧ isAgentInitialCall S c.2 c = true ∨ ¬(isAgentInitialCall S c.1 c = true ∧ isAgentInitialCall S c.2 c = true)

All calls in S are initial for both agents or for neither

theorem final_both_or_neither {m : ℕ} (S : List (Call m)) (c : Call m) : c ∈ S → isAgentFinalCall S c.1 c = true ∧ isAgentFinalCall S c.2 c = true ∨ ¬(isAgentFinalCall S c.1 c = true ∧ isAgentFinalCall S c.2 c = true)

All calls in S are final for both agents or for neither

theorem helper {k n : ℕ} (h : 4 ≤ n) : k ≤ 2 * n - 5 ↔ k < 2 * n - 4

theorem necessity (n : ℕ) : n > 4 → ∀ (σ : List (Call n)), allExpert (after σ) → σ.length ≥ 2 * n - 4

For n ≥ 4 agents, any sequence that makes everyone an expert, has length 2n-4 or higher.