Arbitrarily long order-adherence iterations

noncomputable def OrderClosures.canonicalOrderAdherenceTower {X : Type v} [AddCommGroup X] [Lattice X] (A : Set X) : OrderAdherenceTower A

The canonical transfinite tower obtained by iterating order adherence; used as the tower field of the final global construction.

Equations

• OrderClosures.canonicalOrderAdherenceTower A = { stage := fun (η : Ordinal.{?u.1}) => transfiniteIterate OrderClosures.orderAdherence η A, stage_zero := ⋯, stage_succ := ⋯, stage_limit := ⋯ }

@[reducible, inline]

abbrev OrderClosures.GaoSuccessorGenerator (β : Ordinal.{u}) : Type (u + 1)

A successor-indexed generator type for one Gao component; used to enumerate the initial component stage with controlled cardinality.

Equations

• OrderClosures.GaoSuccessorGenerator β = { ζ : ↑(OrderClosures.GaoIndex β) // ζ ∈ OrderClosures.GaoStageIndices β 1 }

@[reducible, inline]

abbrev OrderClosures.GaoComponentIndex (κ : Cardinal.{u}) : Set Ordinal.{u}

Indices for all Gao components below the successor cardinal of κ; used as the coordinate type of the global product.

Equations

• OrderClosures.GaoComponentIndex κ = Set.Iio (Order.succ κ).ord

@[reducible, inline]

abbrev OrderClosures.GaoComponent (β : Ordinal.{u}) : Type (u + 1)

The continuous-function lattice attached to one Gao ordinal component.

Equations

• OrderClosures.GaoComponent β = C(↑(OrderClosures.GaoCompactSpace β), ℝ)

@[reducible, inline]

abbrev OrderClosures.GaoIterationProduct (κ : Cardinal.{u}) : Type (u + 1)

The padded dependent product containing every required Gao component; used for the global arbitrary-iteration witness.

Equations

• OrderClosures.GaoIterationProduct κ = (((β : ↑(OrderClosures.GaoComponentIndex κ)) → OrderClosures.GaoComponent ↑β) × (ULift.{?u.1 + 1, ?u.1} κ.ord.ToType → ℝ))

instance OrderClosures.instIsOrderedAddMonoidGaoIterationProduct (κ : Cardinal.{u}) : IsOrderedAddMonoid (GaoIterationProduct κ)

Supplies pointwise order compatibility with addition on the iteration product.

instance OrderClosures.instPosSMulMonoRealGaoIterationProduct (κ : Cardinal.{u}) : PosSMulMono ℝ (GaoIterationProduct κ)

Supplies monotonicity of nonnegative scalar multiplication on the iteration product, needed for its vector-lattice structure.

@[instance_reducible]

noncomputable instance OrderClosures.instVectorLatticeGaoIterationProduct (κ : Cardinal.{u}) : VectorLattice (GaoIterationProduct κ)

Bundles the pointwise vector-lattice structure on the padded product.

Equations

• OrderClosures.instVectorLatticeGaoIterationProduct κ = { toModule := Prod.instModule, toPosSMulMono := ⋯ }

theorem OrderClosures.gaoIterationProduct_abs_fst (κ : Cardinal.{u}) (x : GaoIterationProduct κ) (β : ↑(GaoComponentIndex κ)) : |x|.1 β = |x.1 β|

Computes absolute value in the component part of the iteration product; used to analyze solid domination of global generators.

theorem OrderClosures.gaoIterationProduct_abs_snd (κ : Cardinal.{u}) (x : GaoIterationProduct κ) (a : ULift.{u + 1, u} κ.ord.ToType) : |x|.2 a = |x.2 a|

Computes absolute value in the padding coordinate of the iteration product; used to recover generator indices from domination.

theorem OrderClosures.mk_gaoSuccessorGenerator_le (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : Ordinal.{u}) (hβ : β < (Order.succ κ).ord) : Cardinal.mk (GaoSuccessorGenerator β) ≤ Cardinal.lift.{u + 1, u} κ

Bounds the cardinality of the chosen successor-generator type; used to fit all component generators into the global cardinal κ.

noncomputable def OrderClosures.gaoGeneratorEmbedding (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : Ordinal.{u}) (hβ : β < (Order.succ κ).ord) : GaoSuccessorGenerator β ↪ ULift.{u + 1, u} κ.ord.ToType

Embeds a successor-stage generator into the corresponding continuous- function component; used to form the global diagonal family.

Equations

• OrderClosures.gaoGeneratorEmbedding κ hκ β hβ = Classical.choice ⋯

noncomputable def OrderClosures.gaoComponentGenerator (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) (a : ULift.{u + 1, u} κ.ord.ToType) : GaoComponent ↑β

Adds the padding coordinate to a component generator so different indices remain distinguishable under solid domination.

Equations

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

theorem OrderClosures.gaoComponentGenerator_embedding (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) (ζ : GaoSuccessorGenerator ↑β) : gaoComponentGenerator κ hκ β ((gaoGeneratorEmbedding κ hκ ↑β ⋯) ζ) = ordinalProjection ↑β ↑ζ

Evaluates a component generator after embedding into the padded product; used to relate global generators to their Gao coordinates.

noncomputable def OrderClosures.gaoGlobalGenerator (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (a : ULift.{u + 1, u} κ.ord.ToType) : GaoIterationProduct κ

The diagonal generator in the full product for a fixed cardinal index; its range generates the global solid set.

Equations

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

def OrderClosures.gaoProductProjection (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) : GaoIterationProduct κ → GaoComponent ↑β

Projection from the global product to one continuous-function component; used to transfer adherence membership downward.

Equations

• OrderClosures.gaoProductProjection κ β x = x.1 β

noncomputable def OrderClosures.gaoProductInclusion (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) : GaoComponent ↑β → GaoIterationProduct κ

Single-coordinate inclusion of a Gao component into the padded product; used to lift adherence witnesses upward.

Equations

• OrderClosures.gaoProductInclusion κ β x = (Pi.single β x, 0)

theorem OrderClosures.orderConvergesTo_gaoProductProjection (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) {i : Type v} [Preorder i] {f : i → GaoIterationProduct κ} {x : GaoIterationProduct κ} (hfx : OrderConvergesTo f x) : OrderConvergesTo (fun (j : i) => gaoProductProjection κ β (f j)) (gaoProductProjection κ β x)

Shows that coordinate projection preserves order convergence; used to project every global adherence stage to its component stage.

theorem OrderClosures.orderConvergesTo_gaoProductInclusion (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) {i : Type v} [Preorder i] {f : i → GaoComponent ↑β} {x : GaoComponent ↑β} (hfx : OrderConvergesTo f x) : OrderConvergesTo (fun (j : i) => gaoProductInclusion κ β (f j)) (gaoProductInclusion κ β x)

Shows that single-coordinate inclusion preserves order convergence; used to lift component adherence witnesses into the global product.

theorem OrderClosures.gaoProductProjection_orderAdherence (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) (A : Set (GaoIterationProduct κ)) : gaoProductProjection κ β '' orderAdherence A ⊆ orderAdherence (gaoProductProjection κ β '' A)

Transfers membership in order adherence through product projection; used in the inductive comparison of global and component stages.

theorem OrderClosures.gaoProductInclusion_orderAdherence (κ : Cardinal.{u}) (β : ↑(GaoComponentIndex κ)) (A : Set (GaoComponent ↑β)) : gaoProductInclusion κ β '' orderAdherence A ⊆ orderAdherence (gaoProductInclusion κ β '' A)

Transfers component order-adherence membership through coordinate inclusion; used for the reverse stage comparison.

noncomputable def OrderClosures.gaoIterationSet (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : Set (GaoIterationProduct κ)

The solid hull of the global diagonal generator range; this is the set whose adherence tower has the prescribed length.

Equations

• OrderClosures.gaoIterationSet κ hκ = OrderClosures.solidHull (Set.range (OrderClosures.gaoGlobalGenerator κ hκ))

theorem OrderClosures.gaoComponentGenerator_mem (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) (a : ULift.{u + 1, u} κ.ord.ToType) : gaoComponentGenerator κ hκ β a ∈ GaoStageSet (↑β) 1

Places each embedded component generator in the global solid generator set; this initializes the stage-inclusion induction.

theorem OrderClosures.gaoProjection_initial (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) : gaoProductProjection κ β '' gaoIterationSet κ hκ ⊆ GaoStageSet (↑β) 1

Proves the initial projection inclusion between the global set and a Gao component; used as the base case of gaoProjection_stage.

theorem OrderClosures.gaoInclusion_initial (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) : gaoProductInclusion κ β '' GaoStageSet (↑β) 1 ⊆ gaoIterationSet κ hκ

Proves the initial inclusion of a component Gao stage into the global solid set; used as the base case of gaoInclusion_stage.

theorem OrderClosures.gaoProjection_stage (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) (η : Ordinal.{u + 1}) : gaoProductProjection κ β '' (canonicalOrderAdherenceTower (gaoIterationSet κ hκ)).stage η ⊆ (canonicalOrderAdherenceTower (GaoStageSet (↑β) 1)).stage η

Propagates the projection inclusion through every adherence stage; used to transfer component strictness to the global tower.

theorem OrderClosures.gaoInclusion_stage (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (β : ↑(GaoComponentIndex κ)) (η : Ordinal.{u + 1}) : gaoProductInclusion κ β '' (canonicalOrderAdherenceTower (GaoStageSet (↑β) 1)).stage η ⊆ (canonicalOrderAdherenceTower (gaoIterationSet κ hκ)).stage η

Propagates component inclusion through every adherence stage; paired with gaoProjection_stage to compare the two towers.

theorem OrderClosures.one_add_le_add_one_ordinal (δ : Ordinal.{u}) : 1 + δ ≤ δ + 1

Supplies the ordinal successor inequality needed to choose the component whose strict stage witnesses a prescribed global stage.

theorem OrderClosures.gaoIterationTower_strict (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (η : Ordinal.{u + 1}) : η < Ordinal.lift.{u + 1, u} (Order.succ κ).ord → (canonicalOrderAdherenceTower (gaoIterationSet κ hκ)).stage η ⊂ (canonicalOrderAdherenceTower (gaoIterationSet κ hκ)).stage (Order.succ η)

Transfers strictness from a suitable Gao component to every stage below the target ordinal of the global iteration tower.

theorem OrderClosures.gaoGlobalGenerator_index_eq_of_abs_le (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) {a b : ULift.{u + 1, u} κ.ord.ToType} (hab : |gaoGlobalGenerator κ hκ a| ≤ |gaoGlobalGenerator κ hκ b|) : a = b

Recovers equality of generator indices from solid domination; used to prove injectivity of the global generator map.

theorem OrderClosures.gaoGlobalGenerator_injective (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : Function.Injective (gaoGlobalGenerator κ hκ)

Proves that distinct indices give distinct global generators; used for the lower bound on the generator cardinal.

theorem OrderClosures.mk_gaoGlobalGenerator_range (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : Cardinal.mk ↑(Set.range (gaoGlobalGenerator κ hκ)) = Cardinal.lift.{u + 1, u} κ

Computes the cardinality of the global generator range; used in the exact calculation of solidGeneratorNumber.

theorem OrderClosures.solidGeneratorNumber_gaoIterationSet (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) : solidGeneratorNumber (gaoIterationSet κ hκ) = Cardinal.lift.{u + 1, u} κ

Proves that the constructed solid set has generator number exactly κ; used in the final arbitrary-iteration theorem.

theorem OrderClosures.solid_sets_require_arbitrarily_many_iterations (κ : Cardinal.{u}) (hκ : Cardinal.aleph0 ≤ κ) (ξ : Ordinal.{u}) (hξ : ξ ≤ (Order.succ κ).ord) : ∃ (X : Type (u + 1)) (x : AddCommGroup X) (x_1 : Lattice X) (x_2 : IsOrderedAddMonoid X) (x_3 : VectorLattice X) (S : Set X), LatticeOrderedAddCommGroup.IsSolid S ∧ solidGeneratorNumber S = Cardinal.lift.{u + 1, u} κ ∧ NeedsOrderAdherenceIterations S (Ordinal.lift.{u + 1, u} ξ)

Paper Theorem thm:solid-iterations: constructs solid sets requiring any prescribed admissible number of order-adherence iterations.

theorem OrderClosures.orderConvergesTo_zero_of_abs_le_gao {X : Type u} [AddCommGroup X] [Lattice X] {i : Type v} [Preorder i] {f g : i → X} (hg : OrderConvergesTo g 0) (hfg : ∀ (j : i), |f j| ≤ |g j|) : OrderConvergesTo f 0

Converts an absolute-value bound by an order-null net into order convergence to zero; used in solid_generated_orderAdherence.

theorem OrderClosures.solid_generated_orderAdherence {X : Type u} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [VectorLattice X] {G : Set X} (hG : G ⊆ Set.Ici 0) : orderAdherence (solidHull G) = {x : X | ∃ (ι : Type u) (x_1 : Preorder ι) (_ : IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2) (_ : Nonempty ι) (a : ι → X), (∀ (i : ι), a i ∈ G) ∧ OrderConvergesTo (fun (i : ι) => |x| ⊓ a i) |x| ∧ IsLUB (Set.range fun (i : ι) => |x| ⊓ a i) |x|}

Paper Lemma lem:solid-generated-order-adh.