The least Berkeley cardinal rank-reflects a Reinhardt cardinal
DisprovedBagaria.berkeley_reflects_reinhardtTheorem of slide 14, Reinhardt half: if δ₀ is the least Berkeley cardinal in a universe satisfying ZF, then some ordinal γ below δ₀ carries a rank segment that satisfies ZF and contains a Reinhardt cardinal. The source moreover obtains an ω-huge cardinal above κ_ω(j); that clause is not formalized here.
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 14, Reinhardt half: the least Berkeley cardinal
strongly rank-reflects a Reinhardt cardinal. If δ0 is the least Berkeley
cardinal, then some ordinal γ below δ0 carries a rank segment that
satisfies ZF and contains a Reinhardt cardinal. The source obtains the
conclusion together with an ω-huge cardinal above κ_ω(j); that clause is
not formalized here. -/
theorem berkeley_reflects_reinhardt (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(δ0 : Ordinal.{v}) (hB : U.berkeley δ0)
(hL : ∀ δ : Ordinal.{v}, δ < δ0 → ¬ U.berkeley δ) :
∃ γ : Ordinal.{v}, γ < δ0 ∧ SatisfiesZF (U.segmentMem γ) ∧ U.hasReinhardtIn γ := 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, with no smaller ordinal Berkeley, there is an ordinal γ below δ0 such that the rank segment below γ satisfies ZF and contains a Reinhardt cardinal — some non-identity elementary self-embedding of that segment moves the code of some ordinal below γ while fixing all smaller codes. Only the Reinhardt half of slide 14 is captured; the ω-huge cardinal clause of the source is not encoded.