Erdős problem 621
Let be a graph on vertices, be the maximum number of edges that contain at most one edge from every triangle, and be the minimum number of edges that contain at least one edge from every triangle.
Sources
FormalConjectures/ErdosProblems/
621.lean
Let be a graph on vertices, be the maximum number of edges that contain at most one edge from every triangle, and be the minimum number of edges that contain at least one edge from every triangle.
Is it true that
A problem of Erdős, Gallai, and Tuza [EGT96], who observe that this is probably quite difficult since there are different examples where equality hold: the complete graph, the complete bipartite graph, and the graph obtained from by adding one vertex joined to every other.
This is true, and was proved by Norin and Sun [NoSu16], who in fact proved thatwhere is the minimum number of edges that need to be removed to make the graph bipartite.
Here and are taken over subsets of the edge set of , and the inequality is stated multiplied through by so that it lives in the natural numbers.
The linked file states as the least number of edges whose deletion leaves triangle-free, which is the same as meeting every triangle of , and quantifies over an arbitrary Fintype V rather than Fin n.
True ↔ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (a t : ℕ), IsGreatest {k | ∃ A ⊆ G.edgeFinset, A.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → ({s(x, y), s(y, z), s(x, z)} ∩ A).card ≤ 1} a → IsLeast {k | ∃ T ⊆ G.edgeFinset, T.card = k ∧ ∀ (x y z : Fin n), G.Adj x y → G.Adj y z → G.Adj x z → (T ∩ {s(x, y), s(y, z), s(x, z)}).Nonempty} t → 4 * (a + t) ≤ n ^ 2