Density of 5/2-critical graphs

A graph G is 5/2-critical if G has no circular 5/2-coloring (or equivalently, homomorphism to C_5), but every proper subgraph of G has one. We prove that every 5/2-critical graph on n>=4 vertices has at least (5n-2)/4 edges, and list all 5/2-critical graphs achieving this bound. This implies that every planar or projective-planar graph of girth at least 10 is 5/2-colorable.