A super Reinhardt cardinal strongly rank-reflects a Reinhardt cardinal
OpenBagaria.super_reinhardt_reflectsTheorem of slide 11: if κ is a super Reinhardt cardinal in a universe satisfying ZF, then some ordinal γ below κ carries a rank segment that itself satisfies ZF and contains a Reinhardt cardinal. The consistency strength chain CON(totally Reinhardt) implies CON(super Reinhardt) implies CON(Reinhardt) is read off from such reflection statements.
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 11: a super Reinhardt cardinal strongly rank-reflects
a Reinhardt cardinal. If κ is super Reinhardt, then some ordinal γ below κ
carries a rank segment that satisfies ZF and contains a Reinhardt
cardinal — the first-order approximation of ⟨V_γ, V_{γ+1}⟩ satisfying ZF₂
together with "There exists a Reinhardt cardinal". -/
theorem super_reinhardt_reflects (U : Universe.{v}) (hZF : SatisfiesZF U.mem)
(κ : Ordinal.{v}) (h : U.isSuperReinhardt κ) :
∃ γ : Ordinal.{v}, γ < κ ∧ 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 κ that is super Reinhardt — for every ordinal λ there is a non-identity elementary self-map of U whose least moved ordinal code is κ and which sends the code of κ to the code of some ordinal above λ — there is an ordinal γ below κ 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 κ' below γ while fixing the codes of all smaller ordinals in the segment.