Limit club Berkeley cardinals reflect a Berkeley cardinal that is super Reinhardt
OpenBagaria.limit_club_berkeley_segmentTheorem of slide 16, the mission's goal: if δ is a limit club Berkeley cardinal in a universe satisfying ZF, then some δ' below δ is a Berkeley cardinal and is super Reinhardt within the rank segment below δ — the formal counterpart of ⟨V_δ, V_{δ+1}⟩ satisfying "There is a Berkeley card. that is super Reinhardt".
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 16 — the mission's goal: every limit club Berkeley
cardinal reflects a Berkeley cardinal that is super Reinhardt within its
own rank segment. If δ is a limit club Berkeley cardinal, then some δ'
below δ is a Berkeley cardinal and is super Reinhardt within the segment
below δ — the formal counterpart of ⟨V_δ, V_{δ+1}⟩ satisfying "There is a
Berkeley card. that is super Reinhardt". -/
theorem limit_club_berkeley_segment (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(δ : Ordinal.{v}) (h : U.limitClubBerkeley δ) :
∃ δ' : Ordinal.{v}, δ' < δ ∧ U.berkeleyBelow δ δ' ∧ U.superReinhardtIn δ δ' := 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 limit club Berkeley — club Berkeley, and for every ν below δ some Berkeley cardinal lies strictly between ν and δ — there is an ordinal δ' below δ that is itself a Berkeley cardinal and is super Reinhardt within the rank segment below δ: for every ordinal λ below δ there is a non-identity elementary self-embedding of the segment below δ with critical point δ' whose value at the code of δ' is the code of an ordinal above λ. The Berkeley conjunct is the ambient property; the super Reinhardt conjunct is relativized within the segment, mirroring the two conjuncts of the source's model-theoretic formulation.