Please read the file main_engine.tex Formalize and prove Theorem~\ref{thm:main}, Lemma~\ref{lem:proximity} and Corollary~\ref{cor:density}. The proof must be fully sorry-free. Do not add axioms or leave stray sorrys.