The least proto-Berkeley cardinal is Berkeley
OpenBagaria.proto_least_is_berkeleyTheorem of slide 12: if δ₀ is the least proto-Berkeley cardinal in a universe satisfying ZF, then δ₀ is already a Berkeley cardinal: for every transitive set containing δ₀ and every η below δ₀ there is a non-trivial elementary self-embedding of the transitive set whose critical point lies strictly between η and δ₀.
import Mathlib import Definitions.Def_Bagaria_arena import Definitions.Def_Bagaria_reinhardt import Definitions.Def_Bagaria_berkeley
universe v
namespace Bagaria
open Universe
/-- Theorem of slide 12: the least proto-Berkeley cardinal is Berkeley. If
δ0 is proto-Berkeley and no smaller ordinal is, then every transitive set
containing the code of δ0 and every η below δ0 admit a non-trivial
elementary self-embedding of the transitive set whose critical point lies
strictly between η and δ0. -/
theorem proto_least_is_berkeley (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(δ0 : Ordinal.{v}) (hP : U.protoBerkeley δ0)
(hL : ∀ δ : Ordinal.{v}, δ < δ0 → ¬ U.protoBerkeley δ) :
U.berkeley δ0 := by
sorry
end Bagaria
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: given a universe U satisfying ZF and an ordinal δ0 that is proto-Berkeley — every transitive set containing the code of δ0 carries a non-identity elementary self-embedding whose critical point, the least moved ordinal code belonging to the transitive set, is below δ0 — and assuming no smaller ordinal is proto-Berkeley, then δ0 is Berkeley: every transitive set containing the code of δ0 and every η below δ0 admit a non-identity elementary self-embedding of the transitive set whose critical point lies strictly between η and δ0.