No extendible cardinal lies at or below the least Berkeley cardinal
ProvedBagaria.no_extendible_below_least_berkeleyCorollary of slide 13: if δ₀ is the least Berkeley cardinal in a universe satisfying ZF, then no extendible cardinal lies at or below δ₀. Being Berkeley is a Π₂ property, so no Σ₃-correct cardinal can lie at or below the first Berkeley cardinal; in particular extendibility fails there. The formalization captures the extendible corollary; the Σ₃-correctness clause is out of scope.
import Mathlib import Definitions.Def_Bagaria_arena import Definitions.Def_Bagaria_reinhardt import Definitions.Def_Bagaria_berkeley
universe v
namespace Bagaria
open Universe
/-- Corollary of slide 13: no extendible cardinal lies at or below the
least Berkeley cardinal. Being Berkeley is a Π₂ property of the universe,
so no Σ₃-correct cardinal lies at or below the least Berkeley cardinal; in
particular extendibility fails there. The formalization captures the
extendible corollary; the Σ₃-correctness clause is out of scope. -/
theorem no_extendible_below_least_berkeley (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(δ0 : Ordinal.{v}) (hB : U.berkeley δ0)
(hL : ∀ δ : Ordinal.{v}, δ < δ0 → ¬ U.berkeley δ) :
∀ κ : Ordinal.{v}, κ ≤ δ0 → ¬ U.isExtendible κ := 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 Berkeley — every transitive set containing the code of δ0 and every η below δ0 admit a non-identity elementary self-embedding whose critical point lies strictly between η and δ0 — and assuming no smaller ordinal is Berkeley, then for every ordinal κ at or below δ0, κ is not extendible: extendibility would demand, for every ordinal λ above κ, an elementary embedding of the rank segment below λ into some rank segment with critical point κ and with the image of the code of κ being the code of an ordinal above λ; the statement denies this for some λ above each such κ.