def BooleanFourier.IsDictator {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop

def BooleanFourier.IsUnanimous {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop

def BooleanFourier.prefersOver {m : ℕ} (ranking : Equiv.Perm (Fin m)) (a b : Fin m) : Bool

def BooleanFourier.IsArrowViable {n : ℕ} (f : (Fin n → Bool) → Bool) (m : ℕ) : Prop

def BooleanFourier.IsOdd {n : ℕ} (f : (Fin n → Bool) → Bool) : Prop

theorem BooleanFourier.prefersOver_of_lt {m : ℕ} {σ : Equiv.Perm (Fin m)} {a b : Fin m} (h : σ a < σ b) : prefersOver σ a b = true

theorem BooleanFourier.not_prefersOver_of_lt {m : ℕ} {σ : Equiv.Perm (Fin m)} {a b : Fin m} (h : σ b < σ a) : prefersOver σ a b = false

theorem BooleanFourier.exists_perm_placing_at_positions {m : ℕ} (hm : m ≥ 3) (a b c : Fin m) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) : ∃ (σ : Equiv.Perm (Fin m)), σ a = ⟨0, ⋯⟩ ∧ σ b = ⟨1, ⋯⟩ ∧ σ c = ⟨2, ⋯⟩

theorem BooleanFourier.exists_perm_for_valid_triple {m : ℕ} (hm : m ≥ 3) (a b c : Fin m) (hab : a ≠ b) (hbc : b ≠ c) (hac : a ≠ c) (pab pbc pac : Bool) (hvalid : pab = pbc → pac = pab) : ∃ (σ : Equiv.Perm (Fin m)), prefersOver σ a b = pab ∧ prefersOver σ b c = pbc ∧ prefersOver σ a c = pac

theorem BooleanFourier.arrow_viable_subcube {n m : ℕ} (hm : m ≥ 3) (f : (Fin n → Bool) → Bool) (hviable : IsArrowViable f m) (u v w : Fin n → Bool) (hfu : f u = true) (hfv : f v = true) (hw : ∀ (k : Fin n), u k = v k → w k = u k) : f w = true

theorem BooleanFourier.arrow_viable_implies_unique_pivot {n m : ℕ} (hm : m ≥ 3) (f : (Fin n → Bool) → Bool) (hviable : IsArrowViable f m) (hodd : IsOdd f) (i j : Fin n) (hi : BooleanFourier.influence✝ f i > 0) (hj : BooleanFourier.influence✝¹ f j > 0) : i = j

theorem BooleanFourier.arrow_impossibility {n m : ℕ} (hm : m ≥ 3) (f : (Fin n → Bool) → Bool) (hunanimous : IsUnanimous f) (hodd : IsOdd f) (hviable : IsArrowViable f m) : IsDictator f