Zero sharp

0^# (zero sharp) exists iff there exists a non-trivial elementary embedding j : L → L for the constructible Gödel universe L.