Documentation

ConNF.BaseType.Params

Parameters of the construction #

We describe the various parameters to the model construction.

class ConNF.Params :

Type (u + 1)

The parameters of the construction. We collect them all in one class for simplicity. Note that the ordinal λ in the paper is instead referred to here as Λ, since the symbol λ is used for lambda abstractions.

Ordinals and cardinals are represented here as arbitrary types (not sets) with certain properties. For instance, Λ is an arbitrary type that has an ordering <, which is assumed to be a well-ordering (the Λ_isWellOrder term is a proof of this fact).

The prefix # denotes the cardinality of a type.

Λ : Type u
The type indexing the levels of our model. This type is well-ordered. We inductively construct each type level by induction over Λ. Its cardinality is smaller than κ and μ.
Λ_linearOrder : LinearOrder ConNF.Λ
Λ_isWellOrder : IsWellOrder ConNF.Λ fun (x x_1 : ConNF.Λ) => x < x_1
Λ_zero : Zero ConNF.Λ
Λ_succ : SuccOrder ConNF.Λ
Λ_zero_le : ∀ (α : ConNF.Λ), 0 ≤ α
Λ_isLimit : (Ordinal.type fun (x x_1 : ConNF.Λ) => x < x_1).IsLimit
κ : Type u
The type indexing the atoms in each litter. It is well-ordered, has regular cardinality, and is larger than Λ but smaller than κ. It also has an additive monoid structure induced by its well-ordering.
κ_linearOrder : LinearOrder ConNF.κ
κ_isWellOrder : IsWellOrder ConNF.κ fun (x x_1 : ConNF.κ) => x < x_1
κ_ord : (Ordinal.type fun (x x_1 : ConNF.κ) => x < x_1) = (Cardinal.mk ConNF.κ).ord
κ_isRegular : (Cardinal.mk ConNF.κ).IsRegular
κ_succ : SuccOrder ConNF.κ
κ_addMonoid : AddMonoid ConNF.κ
κ_sub : Sub ConNF.κ
κ_add_typein : ∀ (i j : ConNF.κ), Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) (i + j) = Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i + Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) j
κ_sub_typein : ∀ (i j : ConNF.κ), Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) (i - j) = Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i - Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) j
Λ_lt_κ : Cardinal.mk ConNF.Λ < Cardinal.mk ConNF.κ
μ : Type u
A large type used in indexing the litters. This type is well-ordered. Its cardinality is a strong limit, larger than Λ and κ. The cofinality of the order type of μ is at least κ.
μ_linearOrder : LinearOrder ConNF.μ
μ_isWellOrder : IsWellOrder ConNF.μ fun (x x_1 : ConNF.μ) => x < x_1
μ_ord : (Ordinal.type fun (x x_1 : ConNF.μ) => x < x_1) = (Cardinal.mk ConNF.μ).ord
μ_isStrongLimit : (Cardinal.mk ConNF.μ).IsStrongLimit
κ_lt_μ : Cardinal.mk ConNF.κ < Cardinal.mk ConNF.μ
κ_le_μ_ord_cof : Cardinal.mk ConNF.κ ≤ (Cardinal.mk ConNF.μ).ord.cof

Instances

theorem ConNF.Params.Λ_isWellOrder [self : ConNF.Params] :

IsWellOrder ConNF.Λ fun (x x_1 : ConNF.Λ) => x < x_1

theorem ConNF.Params.Λ_zero_le [self : ConNF.Params] (α : ConNF.Λ) :

0 ≤ α

theorem ConNF.Params.Λ_isLimit [self : ConNF.Params] :

(Ordinal.type fun (x x_1 : ConNF.Λ) => x < x_1).IsLimit

theorem ConNF.Params.κ_isWellOrder [self : ConNF.Params] :

IsWellOrder ConNF.κ fun (x x_1 : ConNF.κ) => x < x_1

theorem ConNF.Params.κ_ord [self : ConNF.Params] :

(Ordinal.type fun (x x_1 : ConNF.κ) => x < x_1) = (Cardinal.mk ConNF.κ).ord

theorem ConNF.Params.κ_isRegular [self : ConNF.Params] :

(Cardinal.mk ConNF.κ).IsRegular

theorem ConNF.Params.κ_add_typein [self : ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) (i + j) = Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i + Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) j

theorem ConNF.Params.κ_sub_typein [self : ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) (i - j) = Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i - Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) j

theorem ConNF.Params.Λ_lt_κ [self : ConNF.Params] :

Cardinal.mk ConNF.Λ < Cardinal.mk ConNF.κ

theorem ConNF.Params.μ_isWellOrder [self : ConNF.Params] :

IsWellOrder ConNF.μ fun (x x_1 : ConNF.μ) => x < x_1

theorem ConNF.Params.μ_ord [self : ConNF.Params] :

(Ordinal.type fun (x x_1 : ConNF.μ) => x < x_1) = (Cardinal.mk ConNF.μ).ord

theorem ConNF.Params.μ_isStrongLimit [self : ConNF.Params] :

(Cardinal.mk ConNF.μ).IsStrongLimit

theorem ConNF.Params.κ_lt_μ [self : ConNF.Params] :

Cardinal.mk ConNF.κ < Cardinal.mk ConNF.μ

theorem ConNF.Params.κ_le_μ_ord_cof [self : ConNF.Params] :

Cardinal.mk ConNF.κ ≤ (Cardinal.mk ConNF.μ).ord.cof

Explicit parameters #

There exist valid parameters for the model. The smallest such parameters are

Λ := ℵ_0
κ := ℵ_1
μ = ℶ_{ω_1}.

We begin by creating a few instances that allow us to use cardinals to satisfy the model parameters.

theorem ConNF.noMaxOrder_of_ordinal_type_eq {α : Type u} [Preorder α] [Infinite α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1).IsLimit) :

noncomputable def ConNF.succOrderOfIsWellOrder {α : Type u} [Preorder α] [Infinite α] [inst : IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1).IsLimit) :

Equations

ConNF.succOrderOfIsWellOrder h = { succ := ⋯.succ, le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯, le_of_lt_succ := ⋯ }

Instances For

theorem ConNF.typein_add_lt_of_type_eq_ord {α : Type u_1} [Infinite α] [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1) = (Cardinal.mk α).ord) (x : α) (y : α) :

Ordinal.typein (fun (x x_1 : α) => x < x_1) x + Ordinal.typein (fun (x x_1 : α) => x < x_1) y < Ordinal.type fun (x x_1 : α) => x < x_1

noncomputable def ConNF.add_of_type_eq_ord {α : Type u_1} [Infinite α] [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1) = (Cardinal.mk α).ord) :

Add α

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def IsWellFounded.bot (α : Type u_1) [Nonempty α] (r : α → α → Prop) [i : IsWellFounded α r] :

α

Equations

IsWellFounded.bot α r = ⋯.min Set.univ ⋯

Instances For

theorem IsWellFounded.not_lt_bot (α : Type u_1) [Nonempty α] (r : α → α → Prop) [IsWellFounded α r] (x : α) :

¬r x (IsWellFounded.bot α r)

theorem Ordinal.typein_eq_zero_iff {α : Type u_1} {r : α → α → Prop} [Nonempty α] [IsWellOrder α r] {x : α} :

Ordinal.typein r x = 0 ↔ ∀ (y : α), y ≠ x → r x y

theorem Ordinal.typein_bot {α : Type u_1} [Nonempty α] [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] :

Ordinal.typein (fun (x x_1 : α) => x < x_1) (IsWellFounded.bot α fun (x x_1 : α) => x < x_1) = 0

noncomputable def ConNF.addZeroClass_of_type_eq_ord {α : Type u_1} [Infinite α] [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1) = (Cardinal.mk α).ord) :

AddZeroClass α

Equations

ConNF.addZeroClass_of_type_eq_ord h = let __spread.0 := ConNF.add_of_type_eq_ord h; AddZeroClass.mk ⋯ ⋯

Instances For

noncomputable def ConNF.addMonoid_of_type_eq_ord {α : Type u_1} [Infinite α] [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] (h : (Ordinal.type fun (x x_1 : α) => x < x_1) = (Cardinal.mk α).ord) :

Equations

ConNF.addMonoid_of_type_eq_ord h = let __spread.0 := ConNF.addZeroClass_of_type_eq_ord h; AddMonoid.mk ⋯ ⋯ nsmulRec ⋯ ⋯

Instances For

noncomputable def ConNF.sub_of_isWellOrder {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x x_1 : α) => x < x_1] :

Sub α

Equations

One or more equations did not get rendered due to their size.

Instances For

noncomputable def ConNF.minimalParams :

The smallest set of valid parameters for the model. They are instantiated in Lean's minimal universe 0.

Equations

One or more equations did not get rendered due to their size.

Instances For

Here, we unpack the hypotheses on Λ, κ, μ into instances that Lean can see.

theorem ConNF.aleph0_le_mk_Λ [ConNF.Params] :

Cardinal.aleph0 ≤ Cardinal.mk ConNF.Λ

theorem ConNF.mk_Λ_ne_zero [ConNF.Params] :

Cardinal.mk ConNF.Λ ≠ 0

instance ConNF.instLinearOrderΛ [ConNF.Params] :

LinearOrder ConNF.Λ

Equations

ConNF.instLinearOrderΛ = ConNF.Params.Λ_linearOrder

instance ConNF.instIsWellOrderΛLt [ConNF.Params] :

IsWellOrder ConNF.Λ fun (x x_1 : ConNF.Λ) => x < x_1

Equations

⋯ = ⋯

instance ConNF.instZeroΛ [ConNF.Params] :

Zero ConNF.Λ

Equations

ConNF.instZeroΛ = ConNF.Params.Λ_zero

instance ConNF.instInhabitedΛ [ConNF.Params] :

Inhabited ConNF.Λ

Equations

ConNF.instInhabitedΛ = { default := 0 }

instance ConNF.instInfiniteΛ [ConNF.Params] :

Infinite ConNF.Λ

Equations

⋯ = ⋯

instance ConNF.instSuccOrderΛ [ConNF.Params] :

SuccOrder ConNF.Λ

Equations

ConNF.instSuccOrderΛ = ConNF.Params.Λ_succ

instance ConNF.instNoMaxOrderΛ [ConNF.Params] :

NoMaxOrder ConNF.Λ

Equations

⋯ = ⋯

instance ConNF.instLinearOrderκ [ConNF.Params] :

LinearOrder ConNF.κ

Equations

ConNF.instLinearOrderκ = ConNF.Params.κ_linearOrder

instance ConNF.instIsWellOrderκLt [ConNF.Params] :

IsWellOrder ConNF.κ fun (x x_1 : ConNF.κ) => x < x_1

Equations

⋯ = ⋯

instance ConNF.instSuccOrderκ [ConNF.Params] :

SuccOrder ConNF.κ

Equations

ConNF.instSuccOrderκ = ConNF.Params.κ_succ

instance ConNF.instAddMonoidκ [ConNF.Params] :

AddMonoid ConNF.κ

Equations

ConNF.instAddMonoidκ = ConNF.Params.κ_addMonoid

instance ConNF.instSubκ [ConNF.Params] :

Sub ConNF.κ

Equations

ConNF.instSubκ = ConNF.Params.κ_sub

instance ConNF.instInhabitedκ [ConNF.Params] :

Inhabited ConNF.κ

Equations

ConNF.instInhabitedκ = { default := 0 }

instance ConNF.instInfiniteκ [ConNF.Params] :

Infinite ConNF.κ

Equations

⋯ = ⋯

instance ConNF.instNoMaxOrderκ [ConNF.Params] :

NoMaxOrder ConNF.κ

Equations

⋯ = ⋯

instance ConNF.instLinearOrderμ [ConNF.Params] :

LinearOrder ConNF.μ

Equations

ConNF.instLinearOrderμ = ConNF.Params.μ_linearOrder

instance ConNF.instIsWellOrderμLt [ConNF.Params] :

IsWellOrder ConNF.μ fun (x x_1 : ConNF.μ) => x < x_1

Equations

⋯ = ⋯

instance ConNF.instNonemptyμ [ConNF.Params] :

Nonempty ConNF.μ

Equations

⋯ = ⋯

instance ConNF.instInfiniteμ [ConNF.Params] :

Infinite ConNF.μ

Equations

⋯ = ⋯

instance ConNF.instNoMaxOrderμ [ConNF.Params] :

NoMaxOrder ConNF.μ

Equations

⋯ = ⋯

The ordered structure on `κ` #

def ConNF.κ_ofNat [ConNF.Params] :

ℕ → ConNF.κ

Equations

ConNF.κ_ofNat 0 = 0
ConNF.κ_ofNat n.succ = Order.succ (ConNF.κ_ofNat n)

Instances For

instance ConNF.instOfNatκ [ConNF.Params] (n : ℕ) :

OfNat ConNF.κ n

Equations

ConNF.instOfNatκ n = { ofNat := ConNF.κ_ofNat n }

instance ConNF.instCovariantClassκHAddLe [ConNF.Params] :

CovariantClass ConNF.κ ConNF.κ (fun (x x_1 : ConNF.κ) => x + x_1) fun (x x_1 : ConNF.κ) => x ≤ x_1

Equations

⋯ = ⋯

instance ConNF.instCovariantClassκSwapHAddLe [ConNF.Params] :

CovariantClass ConNF.κ ConNF.κ (Function.swap fun (x x_1 : ConNF.κ) => x + x_1) fun (x x_1 : ConNF.κ) => x ≤ x_1

Equations

⋯ = ⋯

instance ConNF.instContravariantClassκHAddLe [ConNF.Params] :

ContravariantClass ConNF.κ ConNF.κ (fun (x x_1 : ConNF.κ) => x + x_1) fun (x x_1 : ConNF.κ) => x ≤ x_1

Equations

⋯ = ⋯

@[simp]

theorem ConNF.κ_typein_zero [ConNF.Params] :

Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) 0 = 0

theorem ConNF.κ_le_zero_iff [ConNF.Params] (i : ConNF.κ) :

i ≤ 0 ↔ i = 0

theorem ConNF.κ_not_lt_zero [ConNF.Params] (i : ConNF.κ) :

¬i < 0

theorem ConNF.κ_pos [ConNF.Params] (i : ConNF.κ) :

0 ≤ i

@[simp]

theorem ConNF.κ_add_eq_zero_iff [ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

i + j = 0 ↔ i = 0 ∧ j = 0

@[simp]

theorem ConNF.κ_succ_typein [ConNF.Params] (i : ConNF.κ) :

Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) (Order.succ i) = Ordinal.typein (fun (x x_1 : ConNF.κ) => x < x_1) i + 1

theorem ConNF.κ_zero_lt_one [ConNF.Params] :

0 < 1

@[simp]

theorem ConNF.κ_lt_one_iff [ConNF.Params] (i : ConNF.κ) :

i < 1 ↔ i = 0

theorem ConNF.κ_le_self_add [ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

i ≤ i + j

theorem ConNF.κ_le_add_self [ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

i ≤ j + i

theorem ConNF.κ_add_sub_cancel [ConNF.Params] (i : ConNF.κ) (j : ConNF.κ) :

i + j - i = j

theorem ConNF.κ_sub_lt_iff [ConNF.Params] {i : ConNF.κ} {j : ConNF.κ} {k : ConNF.κ} (h : j ≤ i) :

i - j < k ↔ i < j + k

theorem ConNF.κ_sub_lt [ConNF.Params] {i : ConNF.κ} {j : ConNF.κ} {k : ConNF.κ} (h₁ : i < j + k) (h₂ : j ≤ i) :

i - j < k

theorem ConNF.κ_lt_sub_iff [ConNF.Params] {i : ConNF.κ} {j : ConNF.κ} {k : ConNF.κ} :

k < i - j ↔ j + k < i

instance ConNF.instIsLeftCancelAddκ [ConNF.Params] :

IsLeftCancelAdd ConNF.κ

Equations

⋯ = ⋯

Type indices #

@[reducible]

def ConNF.TypeIndex [ConNF.Params] :

Either the base type or a proper type index (an element of Λ). The base type is written ⊥.

Equations

ConNF.TypeIndex = WithBot ConNF.Λ

Instances For

Since Λ is well-ordered, so is Λ together with the base type ⊥. This allows well founded recursion on type indices.

instance ConNF.instWellFoundedRelationΛ [ConNF.Params] :

WellFoundedRelation ConNF.Λ

Equations

ConNF.instWellFoundedRelationΛ = IsWellOrder.toHasWellFounded

instance ConNF.instWellFoundedRelationTypeIndex [ConNF.Params] :

WellFoundedRelation ConNF.TypeIndex

Equations

ConNF.instWellFoundedRelationTypeIndex = IsWellOrder.toHasWellFounded

@[simp]

theorem ConNF.mk_typeIndex [ConNF.Params] :

Cardinal.mk ConNF.TypeIndex = Cardinal.mk ConNF.Λ

There are exactly Λ type indices.

theorem ConNF.card_Iio_lt [ConNF.Params] (x : ConNF.μ) :

Cardinal.mk ↑(Set.Iio x) < Cardinal.mk ConNF.μ

Sets of the form {y | y < x} have cardinality < μ.

theorem ConNF.card_Iic_lt [ConNF.Params] (x : ConNF.μ) :

Cardinal.mk ↑(Set.Iic x) < Cardinal.mk ConNF.μ

Sets of the form {y | y ≤ x} have cardinality < μ.