Golomb rulers

DefinitionGolomb ruler lengths#✓fully proved

For a natural number \(m\), the set of Golomb ruler lengths with \(m\) marks consists of the natural numbers \(L\) for which there is a finite Sidon set \(S\) of natural numbers with \(S \subseteq \{0, 1, \dots, L\}\), exactly \(m\) elements, and \(L \in S\). A mark at \(0\) is not required.

For finite sets of integers the Sidon condition is equivalent to all positive pairwise differences being distinct.

def golombRulerLengths (m : ℕ) : Set ℕ :=
  {L | ∃ S : Finset ℕ, S ⊆ range (L + 1) ∧ S.card = m ∧ (S : Set ℕ).IsSidon ∧ L ∈ S}
Uses 1 · Used by 1
Statement usesSidon set
Used byOptimal Golomb ruler length

DefinitionOptimal Golomb ruler length#✓fully proved

For \(m \ge 1\), the optimal Golomb ruler length \(G(m)\) is the infimum in \(\mathbb{N}\) of the set of Golomb ruler lengths with \(m\) marks, that is, of the natural numbers \(L\) such that some \(m\)-element Sidon set of natural numbers contained in \(\{0, 1, \dots, L\}\) contains \(L\); for \(m = 0\) we set \(G(0) = 0\).

For \(m \ge 2\) this is OEIS A003022, the length of a shortest Golomb ruler with \(m\) marks.

noncomputable def optimalGolombLength (m : ℕ) : ℕ :=
  if m < 1 then 0 else sInf (golombRulerLengths m)
Uses 1 · Used by 3
Statement usesGolomb ruler lengths
Used byOptimal Golomb rulers with 3 to 11 marks · Optimal 28-mark Golomb ruler · Optimal 27-mark Golomb ruler

TheoremOptimal Golomb rulers with 3 to 11 marks#●ready to prove

The optimal Golomb ruler lengths with \(m = 3, 4, \dots, 11\) marks are, in order, \(3, 6, 11, 17, 25, 34, 44, 55, 72\).

public theorem_wanted optimalGolombLength_three_to_eleven :
    (List.range 9).map (fun i => optimalGolombLength (i + 3)) =
      [3, 6, 11, 17, 25, 34, 44, 55, 72]
Sources
  • exhaustive searches; OEIS A003022; listed in leansolving/SqueezeBench SqueezeBench/Problems/Golomb/README.md.
Uses 1
Statement usesOptimal Golomb ruler length

TheoremOptimal 27-mark Golomb ruler#●ready to prove

The optimal Golomb ruler length with \(27\) marks is \(553\).

public theorem_wanted optimalGolombLength_twentySeven : optimalGolombLength 27 = 553
Sources
  • distributed.net OGR-27 exhaustive search, completed 2014; OEIS A003022; listed in SqueezeBench SqueezeBench/Problems/Golomb/README.md.
Uses 1
Statement usesOptimal Golomb ruler length

TheoremOptimal 28-mark Golomb ruler#●ready to prove

The optimal Golomb ruler length with \(28\) marks is \(585\).

public theorem_wanted optimalGolombLength_twentyEight : optimalGolombLength 28 = 585
Sources
  • distributed.net OGR-28 exhaustive search, completed 2022; OEIS A003022; listed in SqueezeBench SqueezeBench/Problems/Golomb/README.md.
Uses 1
Statement usesOptimal Golomb ruler length
2 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.