The regular cardinal used for bookkeeping

We use θ = 2^𝔠 for the uniform stage bound and its successor κ = θ⁺ for the recursion. The identities below are precisely the cardinal arithmetic used in the manuscript.

def ScottishBook155.stageCardinal : Cardinal.{u_1}

Uniform cardinal bound for every Banach stage.

Equations

• ScottishBook155.stageCardinal = 2 ^ Cardinal.continuum

noncomputable def ScottishBook155.recursionCardinal : Cardinal.{u_1}

Regular successor cardinal indexing the final recursion.

Equations

• ScottishBook155.recursionCardinal = Order.succ ScottishBook155.stageCardinal

theorem ScottishBook155.aleph0_le_stageCardinal : Cardinal.aleph0 ≤ stageCardinal

theorem ScottishBook155.real_mk_le_stageCardinal : Cardinal.mk ℝ ≤ stageCardinal

theorem ScottishBook155.stageCardinal_power_aleph0 : stageCardinal ^ Cardinal.aleph0 = stageCardinal

theorem ScottishBook155.stageCardinal_lt_recursionCardinal : stageCardinal < recursionCardinal

theorem ScottishBook155.recursionCardinal_isRegular : recursionCardinal.IsRegular

theorem ScottishBook155.aleph0_lt_recursionCardinal : Cardinal.aleph0 < recursionCardinal

@[reducible, inline]

abbrev ScottishBook155.RecursionIndex : Type u_1

A same-universe well-ordered type of recursion indices.

Equations

• ScottishBook155.RecursionIndex = ScottishBook155.recursionCardinal.ord.ToType

@[reducible, inline]

abbrev ScottishBook155.RecursionIndexZero : Type

The recursion index type in the base universe.

Equations

• ScottishBook155.RecursionIndexZero = ScottishBook155.RecursionIndex

instance ScottishBook155.recursionIndexNonempty : Nonempty RecursionIndex

@[instance_reducible]

noncomputable instance ScottishBook155.recursionIndexOrderBot : OrderBot RecursionIndex

Equations

• ScottishBook155.recursionIndexOrderBot = WellFoundedLT.toOrderBot ScottishBook155.RecursionIndex

instance ScottishBook155.recursionIndexNoMaxOrder : NoMaxOrder RecursionIndex

theorem ScottishBook155.mk_recursionIndex : Cardinal.mk RecursionIndex = recursionCardinal

theorem ScottishBook155.initialSegment_mk_lt (i : RecursionIndex) : Cardinal.mk ↑(Set.Iio i) < recursionCardinal

theorem ScottishBook155.initialSegment_mk_le_stageCardinal (i : RecursionIndex) : Cardinal.mk ↑(Set.Iio i) ≤ stageCardinal

theorem ScottishBook155.initialClosedSegment_mk_le (i : RecursionIndex) : Cardinal.mk ↑(Set.Iic i) ≤ stageCardinal

theorem ScottishBook155.tail_mk (i : RecursionIndex) : Cardinal.mk ↑(Set.Ioi i) = recursionCardinal

Every strict tail of the recursion order still has full cardinality.

noncomputable def ScottishBook155.stageEnumeration {X : Type} [Zero X] (hX : Cardinal.mk X ≤ stageCardinal) : RecursionIndex → X

Any inhabited type within the uniform stage bound admits a recursion-indexed enumeration, with repetitions allowed.

Equations

• ScottishBook155.stageEnumeration hX = fun (i : ScottishBook155.RecursionIndex) => if h : i ∈ Set.range ⇑(Classical.choice ⋯) then (Equiv.ofInjective ⇑(Classical.choice ⋯) ⋯).symm ⟨i, h⟩ else 0

theorem ScottishBook155.stageEnumeration_surjective {X : Type} [Zero X] (hX : Cardinal.mk X ≤ stageCardinal) : Function.Surjective (stageEnumeration hX)