Club Berkeley cardinals are totally Reinhardt
DisprovedBagaria.club_berkeley_totally_reinhardtTheorem of slide 15: every club Berkeley cardinal is totally Reinhardt. Regularity plus the requirement that the critical points of the elementary self-embeddings meet every club subset of δ give enough choiceless embedding structure to see every class of the segment below δ as containing an A-super Reinhardt cardinal within the segment.
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 15: every club Berkeley cardinal is totally
Reinhardt. Regularity, plus critical points of the elementary
self-embeddings meeting every club of δ, give enough embedding structure
that the rank segment below δ satisfies ZF and, for every class A of the
segment, contains an A-super Reinhardt cardinal. -/
theorem club_berkeley_totally_reinhardt (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(δ : Ordinal.{v}) (hC : U.clubBerkeley δ) :
U.isTotallyReinhardt δ := 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 δ that is club Berkeley — δ is regular, and every club subset C of δ and every transitive set containing the code of δ carry a non-identity elementary self-embedding of the transitive set whose critical point lies in C — then δ is totally Reinhardt: the rank segment below δ satisfies ZF, and for every class A of that segment there is an ordinal δ' below δ that is A-super Reinhardt within the segment — for every λ below δ there is a non-identity elementary self-embedding of the segment with critical point δ', sending the code of δ' to the code of an ordinal above λ, and fixing A pointwise along the embedding.