Small values of cap set sizes and Roth numbers

TheoremLargest cap set in dimension three#●ready to prove

Let \(\mathbb{F}_3\) be the field with three elements. The largest subset of \(\mathbb{F}_3^3\) containing no three-term arithmetic progression, that is, no elements \(a, b, c\) of the subset with \(a + c = 2b\) and \(a \neq b\), has exactly \(9\) elements.

Over \(\mathbb{F}_3\) these subsets are exactly the caps: sets with no three distinct collinear points.

public theorem_wanted capSet_dim_three :
    addRothNumber (Finset.univ : Finset (Fin 3 → ZMod 3)) = 9
Sources
  • exhaustive search; OEIS A090245; listed in leansolving/SqueezeBench SqueezeBench/Problems/CapSet/README.md.

TheoremLargest cap set in dimension four#●ready to prove

Let \(\mathbb{F}_3\) be the field with three elements. The largest subset of \(\mathbb{F}_3^4\) containing no three-term arithmetic progression, that is, no elements \(a, b, c\) of the subset with \(a + c = 2b\) and \(a \neq b\), has exactly \(20\) elements.

Over \(\mathbb{F}_3\) these subsets are exactly the caps: sets with no three distinct collinear points.

public theorem_wanted capSet_dim_four :
    addRothNumber (Finset.univ : Finset (Fin 4 → ZMod 3)) = 20
Sources
  • G. Pellegrino, Sul massimo ordine delle calotte in S₄,₃, Matematiche (Catania) 25 (1970), 149–157; OEIS A090245; listed in SqueezeBench SqueezeBench/Problems/CapSet/README.md.

TheoremLargest cap set in dimension five#●ready to prove

Let \(\mathbb{F}_3\) be the field with three elements. The largest subset of \(\mathbb{F}_3^5\) containing no three-term arithmetic progression, that is, no elements \(a, b, c\) of the subset with \(a + c = 2b\) and \(a \neq b\), has exactly \(45\) elements.

Over \(\mathbb{F}_3\) these subsets are exactly the caps: sets with no three distinct collinear points.

public theorem_wanted capSet_dim_five :
    addRothNumber (Finset.univ : Finset (Fin 5 → ZMod 3)) = 45
Sources
  • Y. Edel, S. Ferret, I. Landjev, and L. Storme, The classification of the largest caps in AG(5,3), J. Combin. Theory Ser. A 99 (2002), 95–110; OEIS A090245; listed in SqueezeBench SqueezeBench/Problems/CapSet/README.md.

TheoremLargest cap set in dimension six#●ready to prove

Let \(\mathbb{F}_3\) be the field with three elements. The largest subset of \(\mathbb{F}_3^6\) containing no three-term arithmetic progression, that is, no elements \(a, b, c\) of the subset with \(a + c = 2b\) and \(a \neq b\), has exactly \(112\) elements.

Over \(\mathbb{F}_3\) these subsets are exactly the caps: sets with no three distinct collinear points.

public theorem_wanted capSet_dim_six :
    addRothNumber (Finset.univ : Finset (Fin 6 → ZMod 3)) = 112
Sources
  • A. Potechin, Maximal caps in AG(6,3), Des. Codes Cryptogr. 46 (2008), 243–259; OEIS A090245; listed in SqueezeBench SqueezeBench/Problems/CapSet/README.md.

TheoremRoth numbers from five to fourteen#●ready to prove

For a natural number \(n\), let \(r_3(n)\) be the largest size of a subset of \(\{0, 1, \dots, n - 1\}\) containing no three-term arithmetic progression, that is, no elements \(a, b, c\) of the subset with \(a + c = 2b\) and \(a \neq b\). Then the values \(r_3(5), r_3(6), \dots, r_3(14)\) are \(4, 4, 4, 4, 5, 5, 6, 6, 7, 8\), in this order.

public theorem_wanted rothNumberNat_five_to_fourteen :
    (List.range 10).map (fun i => rothNumberNat (i + 5)) = [4, 4, 4, 4, 5, 5, 6, 6, 7, 8]
Sources
  • OEIS A003002; listed in SqueezeBench SqueezeBench/Problems/Roth/README.md.
5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.