Golomb rulers with real marks: the real and integer optima agree up to ten marks

A Golomb ruler is a set of integer marks whose pairwise differences are distinct. We let the marks be real numbers and ask that every difference be at least 1 and that any two differences be at least 1 apart. The least length G_R(n) of such a real ruler with n marks is at most the optimal Golomb length G_Z(n). Fixing the order of all differences splits the problem into finitely many polyhedral chambers. A branch-and-bound over these chambers, with an exact rational certificate at every leaf, proves G_R(n) = G_Z(n) for n ≤ 10; each proof takes under a minute, and an independent checker verifies it in exact arithmetic. An exhaustive exact enumeration of all chamber vertices confirms the result for n ≤ 7 and shows that there the shortest real rulers are exactly the optimal integer rulers and their mirror images. The number of chambers it meets agrees with the number of combinatorial types of real Golomb rulers counted by Beck, Bogart and Pham. Non-integral chamber vertices first appear at n = 7: there are 84, all half-integral. Already there, 80 of them are shortest points of their chambers, 40 of them the only one, although the global optimum is integral; a twelve-mark example of the same kind comes from Singer's construction. The archive contains the branch-and-bound, the proof checker, the six proof files, exact checks of the two examples, certificates for the 84 chambers with their checker, the enumeration programs and all run outputs, with SHA-256 checksums. The checkers use only the Python standard library.