The challenge definitions in terms of edge costs

bipartizationNumber H counts the deletions that make the subgraph H bipartite, while edgeCost minimizes the monochromatic edges over sign assignments. Deleting the monochromatic edges of a sign assignment leaves a bipartite graph, and a 2-coloring of what remains after deleting D leaves every monochromatic edge in D, so the two agree. Hence the hypothesis of the challenge is C-linearity, and every finite edge set of G on n vertices bounds h G n from below.

theorem Erdos111.bipartizationNumber_eq_edgeCost {V : Type u_1} {G : SimpleGraph V} (H : G.Subgraph) (E : Finset (Sym2 V)) (hE : ↑E = H.edgeSet) : bipartizationNumber H = edgeCost E

The number of deletions that make a finite subgraph bipartite is the edge cost of its edge set.

theorem Erdos111.linear_of_bipartizationNumber_le {V : Type u_1} {G : SimpleGraph V} {C : ℝ} (hC : ∀ (H : G.Subgraph), H.verts.Finite → ↑(bipartizationNumber H) ≤ C * ↑H.verts.ncard) : Linear G C.toNNReal

The hypothesis of the challenge is C-linearity.

theorem Erdos111.edgeCost_le_h {V : Type u_1} {G : SimpleGraph V} {s : Finset V} {E : Finset (Sym2 V)} (hE : ↑E ⊆ G.edgeSet) (hEs : ∀ e ∈ E, ∀ v ∈ e, v ∈ s) : edgeCost E ≤ h G s.card

A finite edge set of G with ends in s bounds h G s.card from below.