Planar graphs are 9/2-colorable

We show that every planar graph G has a 2-fold 9-coloring. In particular, this implies that G has fractional chromatic number at most 92. This is the first proof (independent of the 4 Color Theorem) that there exists a constant k<5 such that every planar G has fractional chromatic number at most k.