one Lake project, not one per line

A single Lake project at lean/, library Workspace, with per-line namespaces. The alternative — a project per research line — would have meant a separate dependency pin and a separate toolchain per line, and the first time the two lines shared a definition it would have meant a fourth package to hold it. One project keeps the solver stack consistent by construction.