robertmonjo/BigBangTheorem: Lean files for the Big Bang theorem

This release contains the Lean supplementary material for the article "If the Big Bang exists, the homogeneous Universe is closed". Contents: BigBangTheorem/BigBangTheorem_Strong.lean: formalization of the analytic core of the strong version, based on Lipschitz control of the slice-volume function. BigBangTheorem/BigBangTheorem_Weak.lean: formalization of the analytic core of the weak version, based on finite accumulated expansion. BigBangTheorem.lean: root module importing the strong and weak files. Build: lake build