def
definition
galactic_status
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Gravity.GalacticTimescale on GitHub at line 95.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
92 linarith
93 linarith
94
95def galactic_status : List (String × String) :=
96 [ ("N_galactic approx", "PROVEN")
97 , ("tau_star is phi rung", "PROVEN")
98 ]
99
100#eval galactic_status
101
102end
103end GalacticTimescale
104end Gravity
105end IndisputableMonolith