FormalConjectures.Arxiv.«2104.00502».BarkerSequence

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Barker sequences

A Barker sequence is a finite sequence of $\pm 1$ values whose nontrivial aperiodic autocorrelations all have magnitude at most one. The Barker conjecture says that no such sequence has length greater than $13$.

References:

J. Willms, A note on Barker sequences of even length

Barker code

OEIS A091704

namespace Arxiv.«2104.00502»

The aperiodic autocorrelation $C_k(a)=\sum_i a_i a_{i+k}$.

def aperiodicAutocorrelation (a : List ℤ) (k : ℕ) : ℤ :=
  (List.zipWith (· * ·) a (a.drop k)).sum

A Barker sequence has $\pm 1$ entries and nontrivial autocorrelations of magnitude at most one.

def IsBarkerSequence (a : List ℤ) : Prop :=
  (∀ x ∈ a, x = 1 ∨ x = -1) ∧
    ∀ k : ℕ, 0 < k → k < a.length → |aperiodicAutocorrelation a k| ≤ 1

Every Barker sequence has length at most $13$.

@[category research open, AMS 5 11 94]
theorem barker_conjecture (a : List ℤ) (ha : IsBarkerSequence a) : a.length ≤ 13 := bya:List ℤha:IsBarkerSequence a⊢ a.length ≤ 13
  sorryAll goals completed! 🐙

The known sequence $(1,1,1,1,1,-1,-1,1,1,-1,1,-1,1)$ of length $13$ is a Barker sequence.

@[category test, AMS 5 11 94]
theorem isBarkerSequence_length_thirteen :
    IsBarkerSequence [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] := by⊢ IsBarkerSequence [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1]
  constructorleft⊢ ∀ x ∈ [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1], x = 1 ∨ x = -1right⊢ ∀ (k : ℕ),
  0 < k →
    k < [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1].length →
      |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] k| ≤ 1
  ·left⊢ ∀ x ∈ [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1], x = 1 ∨ x = -1 simpAll goals completed! 🐙
  ·right⊢ ∀ (k : ℕ),
  0 < k →
    k < [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1].length →
      |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] k| ≤ 1 intro k hkpos hklenrightk:ℕhkpos:0 < khklen:k < [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1].length⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] k| ≤ 1
    norm_num at hklenrightk:ℕhkpos:0 < khklen:k < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] k| ≤ 1
    interval_cases kright.«1»k:ℕhkpos:0 < 1hklen:1 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 1| ≤ 1right.«2»k:ℕhkpos:0 < 2hklen:2 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 2| ≤ 1right.«3»k:ℕhkpos:0 < 3hklen:3 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 3| ≤ 1right.«4»k:ℕhkpos:0 < 4hklen:4 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 4| ≤ 1right.«5»k:ℕhkpos:0 < 5hklen:5 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 5| ≤ 1right.«6»k:ℕhkpos:0 < 6hklen:6 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 6| ≤ 1right.«7»k:ℕhkpos:0 < 7hklen:7 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 7| ≤ 1right.«8»k:ℕhkpos:0 < 8hklen:8 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 8| ≤ 1right.«9»k:ℕhkpos:0 < 9hklen:9 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 9| ≤ 1right.«10»k:ℕhkpos:0 < 10hklen:10 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 10| ≤ 1right.«11»k:ℕhkpos:0 < 11hklen:11 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 11| ≤ 1right.«12»k:ℕhkpos:0 < 12hklen:12 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 12| ≤ 1 <;>right.«1»k:ℕhkpos:0 < 1hklen:1 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 1| ≤ 1right.«2»k:ℕhkpos:0 < 2hklen:2 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 2| ≤ 1right.«3»k:ℕhkpos:0 < 3hklen:3 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 3| ≤ 1right.«4»k:ℕhkpos:0 < 4hklen:4 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 4| ≤ 1right.«5»k:ℕhkpos:0 < 5hklen:5 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 5| ≤ 1right.«6»k:ℕhkpos:0 < 6hklen:6 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 6| ≤ 1right.«7»k:ℕhkpos:0 < 7hklen:7 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 7| ≤ 1right.«8»k:ℕhkpos:0 < 8hklen:8 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 8| ≤ 1right.«9»k:ℕhkpos:0 < 9hklen:9 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 9| ≤ 1right.«10»k:ℕhkpos:0 < 10hklen:10 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 10| ≤ 1right.«11»k:ℕhkpos:0 < 11hklen:11 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 11| ≤ 1right.«12»k:ℕhkpos:0 < 12hklen:12 < 13⊢ |aperiodicAutocorrelation [1, 1, 1, 1, 1, -1, -1, 1, 1, -1, 1, -1, 1] 12| ≤ 1
      norm_num [aperiodicAutocorrelation] at hkpos ⊢All goals completed! 🐙

The sequence $(1,1,1,-1)$ is a Barker sequence.

@[category test, AMS 5 11 94]
theorem isBarkerSequence_length_four : IsBarkerSequence [1, 1, 1, -1] := by⊢ IsBarkerSequence [1, 1, 1, -1]
  constructorleft⊢ ∀ x ∈ [1, 1, 1, -1], x = 1 ∨ x = -1right⊢ ∀ (k : ℕ), 0 < k → k < [1, 1, 1, -1].length → |aperiodicAutocorrelation [1, 1, 1, -1] k| ≤ 1
  ·left⊢ ∀ x ∈ [1, 1, 1, -1], x = 1 ∨ x = -1 simpAll goals completed! 🐙
  ·right⊢ ∀ (k : ℕ), 0 < k → k < [1, 1, 1, -1].length → |aperiodicAutocorrelation [1, 1, 1, -1] k| ≤ 1 intro k hkpos hklenrightk:ℕhkpos:0 < khklen:k < [1, 1, 1, -1].length⊢ |aperiodicAutocorrelation [1, 1, 1, -1] k| ≤ 1
    norm_num at hklenrightk:ℕhkpos:0 < khklen:k < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] k| ≤ 1
    interval_cases kright.«1»k:ℕhkpos:0 < 1hklen:1 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 1| ≤ 1right.«2»k:ℕhkpos:0 < 2hklen:2 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 2| ≤ 1right.«3»k:ℕhkpos:0 < 3hklen:3 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 3| ≤ 1 <;>right.«1»k:ℕhkpos:0 < 1hklen:1 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 1| ≤ 1right.«2»k:ℕhkpos:0 < 2hklen:2 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 2| ≤ 1right.«3»k:ℕhkpos:0 < 3hklen:3 < 4⊢ |aperiodicAutocorrelation [1, 1, 1, -1] 3| ≤ 1
      norm_num [aperiodicAutocorrelation] at hkpos ⊢All goals completed! 🐙

The constant sequence $(1,1,1,1)$ is not a Barker sequence.


@[category test, AMS 5 11 94]
theorem not_isBarkerSequence_constant_four : ¬ IsBarkerSequence [1, 1, 1, 1] := by⊢ ¬IsBarkerSequence [1, 1, 1, 1]
  intro haha:IsBarkerSequence [1, 1, 1, 1]⊢ False
  have h := ha.2 1 (byha:IsBarkerSequence [1, 1, 1, 1]⊢ 0 < 1ha:IsBarkerSequence [1, 1, 1, 1]h:|aperiodicAutocorrelation [1, 1, 1, 1] 1| ≤ 1⊢ False norm_numAll goals completed! 🐙ha:IsBarkerSequence [1, 1, 1, 1]h:|aperiodicAutocorrelation [1, 1, 1, 1] 1| ≤ 1⊢ False) (byha:IsBarkerSequence [1, 1, 1, 1]⊢ 1 < [1, 1, 1, 1].lengthha:IsBarkerSequence [1, 1, 1, 1]h:|aperiodicAutocorrelation [1, 1, 1, 1] 1| ≤ 1⊢ False norm_numAll goals completed! 🐙ha:IsBarkerSequence [1, 1, 1, 1]h:|aperiodicAutocorrelation [1, 1, 1, 1] 1| ≤ 1⊢ False)ha:IsBarkerSequence [1, 1, 1, 1]h:|aperiodicAutocorrelation [1, 1, 1, 1] 1| ≤ 1⊢ False
  norm_num [aperiodicAutocorrelation] at hAll goals completed! 🐙

end Arxiv.«2104.00502»