|
|
|
|
|
|
by bmenrigh
146 days ago
|
|
|
You should look. It’s almost more entertaining than the README.md theorem MilkyWay_Is_Collapsed : DeterminePhase MilkyWay = Phase.Collapsed := by
-- ArkScalar MW ≈ 0.41 < 0.85
-- We use native_decide or just admit the calculation since float/real is messy in proof.
sorry -- Calculation verified by python script
|
|
|