Sufficient

We show that for n ≥ 4 agents there is a call sequence of length 2n - 4 that makes each agent learn the secrets of all others (become an expert).

Authors: Timo Doherty, Malvin Gattinger

theorem addAgentEqualsSucc {n : ℕ} : addAgent (initialState n) = initialState n.succ

We can replace addAgent with initialState (n + 1) in the following lemma n ≥ 4.

theorem singleMakeCalls {n : ℕ} (initial_call : Call (n + 1)) (expandedSeq : List (Call (n + 1))) : makeCall (makeCalls (makeCall (addAgent (initialState n)) initial_call) expandedSeq) initial_call = makeCalls (initialState (n + 1)) ([initial_call] ++ expandedSeq ++ [initial_call])

addAgent (initialState n) is replacable with initialState (n + 1) in the following lemma.

theorem addAgentMakeCallCommute {n : ℕ} (c : Call n) (someState : GossipState n) : makeCall (addAgent someState) (match c with | (i, j) => (i.castSucc, j.castSucc)) = addAgent (makeCall someState c)

addAgent and makeCall commute if the call doesn't contain the new agent.

theorem addAgentMakeCallsCommute {n : ℕ} (σ : List (Call n)) (someState : GossipState n) : (makeCalls (addAgent someState) do let a ← σ pure (match a with | (i, j) => (i.castSucc, j.castSucc))) = addAgent (makeCalls someState σ)

addAgent and makeCalls commute if the call sequence doesn't contain the new agent.

theorem twoSecretsSuccSingle {n : ℕ} (s : GossipState (n + 4).succ) (a b : Fin (n + 4).succ) (seq : List (Call (n + 4).succ)) (a_def : a = 0) (b_def : b = Fin.last (n + 4)) (only_ab_know_ab : ∀ (i : Fin (n + 4).succ), i ≠ a ∧ i ≠ b → ¬s i a ∧ ¬s i b) (a_knows_b : s a b) (b_knows_a : s b a) (fin_succ_knows_own : s b b) (k : Fin (n + 4).succ) : makeCalls s seq k a → makeCalls s seq k b

Given that only a knows a and b, then we can show that all agents that learn a also learn b.

theorem twoSecretsSucc {n : ℕ} (s : GossipState (n + 4).succ) (a b : Fin (n + 4).succ) (seq : List (Call (n + 4).succ)) (a_def : a = 0) (b_def : b = Fin.last (n + 4)) (only_ab_know_ab : ∀ (i : Fin (n + 4).succ), i ≠ a ∧ i ≠ b → ¬s i a ∧ ¬s i b) (a_knows_b : s a b) (b_knows_a : s b a) (all_learn_a : ∀ (j : Fin (n + 4).succ), makeCalls s seq j a) (fin_succ_knows_own : s b b) (k : Fin (n + 4).succ) : makeCalls s seq k b

Given that only agent a knows a and b, and some sequence makes everyone else learn a, then everyone else also learns b.

def zero_fin {n : ℕ} : Fin (n + 4).succ

Definitions to avoid repetition.

Equations

• zero_fin = 0

def succ_fin {n : ℕ} : Fin (n + 4).succ

Equations

• succ_fin = Fin.last (n + 4)

def initial_call {k : ℕ} : Call (k + 4).succ

Equations

• initial_call = (zero_fin, succ_fin)

theorem lemma_1 {k : ℕ} (seq : List (Call (k + 4))) (IH : allExpert (makeCalls (initialState (k + 4)) seq)) (i : Fin (k + 4).succ) : i ≠ Fin.last (k + 4) → makeCalls (makeCall (addAgent (initialState (k + 4))) (zero_fin, succ_fin)) (do let a ← seq pure (match a with | (i, j) => (i.castSucc, j.castSucc))) zero_fin i

The first agent learns all old secrets.

theorem lemma_2 {k : ℕ} (seq : List (Call (k + 4))) : makeCalls (makeCall (addAgent (initialState (k + 4))) initial_call) (do let a ← seq pure (match a with | (i, j) => (i.castSucc, j.castSucc))) zero_fin succ_fin

Shows that the first agent learns the new agent's secret.

theorem lemma_3 {k : ℕ} (seq : List (Call (k + 4))) (IH : allExpert (makeCalls (initialState (k + 4)) seq)) : isExpert (makeCalls (makeCall (addAgent (initialState (k + 4))) initial_call) do let a ← seq pure (match a with | (i, j) => (i.castSucc, j.castSucc))) zero_fin

Combining lemma_1 and lemma_2 to show that the first agent is an expert.

theorem inductiveCase (k : ℕ) (seq : List (Call (k + 4))) : allExpert (makeCalls (initialState (k + 4)) seq) → ∃ (seq' : List (Call (k.succ + 4))), seq'.length = 2 + seq.length ∧ allExpert (makeCalls (initialState (k.succ + 4)) seq')

Main lemma for the inductive step.

theorem sufficiency (n : ℕ) : n ≥ 4 → ∃ (seq : List (Call n)), seq.length = 2 * n - 4 ∧ allExpert (makeCalls (initialState n) seq)

Main theorem: for n ≥ 4 agents there exists a sequence of calls that makes everyone an expert.