Глава 1. Метрика на процессах

Зачем Части V нужна метрика

Что осталось позади и что впереди

Часть IV построила процессную математику действительного числа. Бесконечность стала процессом, число — процессом приближений, точка — классом эквивалентных процессов; была доказана несчётность, очерчен процессный континуум, и весь корпус был честно измерен на силу вывода. К концу Части IV в руках оказался материал: рациональные процессы, отношение эквивалентности, аппарат Коши.

Часть V берёт этот материал и принимается за анализ. Её задача — развернуть на процессной основе то, что в классической математике составляет здание математического анализа: топологию, метрику, непрерывность, производную, интеграл. Семь глав Части V пройдут этот путь по порядку — от локального к глобальному, от одной точки к интегрированию по области.

И первый шаг на этом пути — расстояние. Без понятия расстояния не построить ничего дальнейшего: ни топологии (что значит <<близкие>> процессы?), ни сходимости (что значит, что процесс <<приближается>> к чему-то?), ни непрерывности (что значит, что малое смещение аргумента даёт малое смещение значения?). Метрика — фундамент, и потому Часть V открывается главой о ней.

Как читать эту часть: три оговорки

Прежде чем строить, нужно условиться, как Часть V говорит о сделанном, — потому что тут есть опасность, и честнее назвать её сразу.

Соблазн, разворачивая анализ, был бы такой: объявить, что <<классический анализ полностью восстановлен на процессной основе>>. Этот соблазн Часть V отклоняет. Точнее будет сказать иначе: Rocq-репозиторий ToS содержит сеточно-процессную инфраструктуру анализа — рабочий каркас из рациональных метрик, интервальных методов, конечных сумм, модульных оценок и Коши-представителей. Часть V показывает, как этот каркас постепенно восстанавливает классический анализ; и для каждого результата она честно помечает его статус. Отсюда три сквозные оговорки.

Первая — о том, что значит <<процессный анализ>>. Это не готовое здание, а инфраструктура: набор конструкций, в которых аналитические понятия получают процессную форму. Иные результаты в ней уже доказаны как полные теоремы; иные существуют пока как $ε$ -версии, сеточные приближения или конструкции, работающие до конечного горизонта; иные намечены как направление. Часть V эти статусы различает и не выдаёт один за другой.

Вторая — о словах <<без аксиомы выбора>>. Они будут встречаться, и значат они точную вещь: без внешней теоретико-множественной аксиомы выбора и без выбора из завершённых бесконечных семейств. Они не значат, что каждый файл репозитория полностью конструктивен: часть результатов опирается на законы логики ToS — $L 3$ , локально $L 4$ . Статус каждого результата по этой части указывается на месте. (Для настоящей главы, впрочем, оговорка работает в сильную сторону: все её опорные файлы — без единой аксиомы; об этом — ниже.)

Третья — о локальной пометке статуса. Всякий раз, когда глава говорит <<доказано>>, она уточняет, что именно доказано: полная теорема, или $ε$ -приближение, или понятие, введённое определением, или направление дальнейшей работы. Это та же дисциплина честности, что и в Главе 4.6, перенесённая теперь на каждый шаг анализа.

Третий слой изложения

И ещё одно о жанре. Части I–IV держались двух слоёв: формальное построение и онтологическая интерпретация. Часть V добавляет третий — вычислительный. Там, где это уместно, глава будет приводить конкретные примеры вычисления: таблицы, прогоны, числа. Цель проста: читатель должен видеть, что процессный анализ — не отвлечённая абстракция, а работающая практика. В настоящей главе третий слой появится в § 1.7, где архимедовость из философского мотива превратится в конкретную таблицу: сколько шагов довольно, чтобы достичь заданной точности.

Замысел главы

Глава движется от простого к составному. Сначала — расстояние между рациональными числами, простейший случай (§ 1.2). Затем — абстрактное метрическое пространство как общая рамка (§ 1.3). Затем — центральный поворот: поточечное расстояние между процессами естественно само является процессом — процессом рациональных расхождений; и здесь придётся аккуратно отделить его от другой конструкции репозитория — конечногоризонтной дистанции process_dist, измеряющей расхождение до выбранного горизонта (§ 1.4). Далее — общая схема процессов и мосты между их типами (§ 1.5). Отдельный, самый осторожный раздел — о полноте: почему она здесь понятие, а не доказанная теорема (§ 1.6). Затем — архимедовость как <<топливо>> $ε$ -рассуждений, с вычислительным примером (§ 1.7). И наконец — итог: что построено, что нет, что готовится дальше (§ 1.8).

Опорных файлов семь, и все они сверены с репозиторием дословно. Заметим сразу важное: все семь по своим заголовкам и проверенным ключевым теоремам имеют статус <<0 axioms>> — ни одной аксиомы. Для первой главы Части V это удачное начало: фундамент анализа закладывается на полностью конструктивном основании. (Раздел § 1.7 привлечёт дополнительно ещё один файл — об архимедовости; о его статусе там будет сказано отдельно.)

Расстояние между рациональными числами

Простейший случай

Начать стоит с самого простого расстояния, какое только есть в ToS, — расстояния между двумя рациональными числами. Каждое рациональное число конечно как запись: дробь $p / q$ задаётся конечными целыми данными — парой целых (Часть III), и в ней нет ни процесса, ни приближения, ни бесконечности. (Тип $Q$ как таковой, конечно, бесконечен — но речь о каждом отдельном его объекте.) Расстояние между двумя такими числами мы определяем так же просто и завершённо — как модуль их разности: расстояние между рациональными $x$ и $y$ есть $∣ x - y ∣$ . Никакой бесконечности здесь не задействовано — вычитание рациональных и взятие модуля суть конечные операции, и результат снова рационален. В Rocq это записано в файле MetricSpace.v:

Definition Q_dist (x y : Q) : Q := Qabs (x - y).

{ Заметим сразу одну особенность репозитория: то же самое определение встречается в нём под несколькими именами. В ProcessTopMetric.v оно названо qdist, в ProcessGeneral.v — Qdist. Все три — Q_dist, qdist, Qdist — суть одна конструкция: $∣ x - y ∣$ для рациональных $x, y$ . Это не три разных понятия, а одно понятие в трёх файлах. Дальше глава будет пользоваться рабочим именем qdist; читателю достаточно помнить, что за всеми тремя именами стоит один и тот же модуль разности. }

Имя	Файл	Роль
`Q_dist`	`MetricSpace.v`	метрика в `stdlib`-рамке
`qdist`	`ProcessTopMetric.v`	процессно-топологическая метрика
`Qdist`	`ProcessGeneral.v`	расстояние в общей схеме процессов

Все три определены одинаково — Qabs (x - y), — и различаются только тем, в каком файле и для какой цели введены.

Четыре аксиомы метрики

Чтобы $∣ x - y ∣$ заслуживало имени расстояния, оно должно удовлетворять четырём свойствам, которые со времён Фреше составляют определение метрики. И эти четыре свойства мы для рационального расстояния не постулируем, а доказываем — каждое прямой рациональной арифметикой. В MetricSpace.v им отвечают четыре леммы.

Неотрицательность: $∣ x - y ∣ \geq 0$ для любых $x, y$ — расстояние не бывает отрицательным (лемма Q_dist_nonneg).

Нуль на диагонали: $∣ x - x ∣ = 0$ — расстояние от числа до самого себя есть нуль (Q_dist_zero).

Симметрия: $∣ x - y ∣ = ∣ y - x ∣$ — расстояние от $x$ до $y$ и от $y$ до $x$ одно и то же (Q_dist_sym).

Неравенство треугольника: $∣ x - z ∣ \leq ∣ x - y ∣ + ∣ y - z ∣$ — путь напрямую не длиннее пути через промежуточную точку (Q_dist_triangle).

Доказательства просты: все четыре опираются на свойства модуля рационального числа (Qabs) — модуль неотрицателен, модуль нуля есть нуль, модуль не зависит от знака, модуль суммы не превосходит суммы модулей. Все четыре свойства получены чисто рациональной арифметикой, без всякого обращения к бесконечным объектам.

Заметим, чего в этом списке нет. Свойство нуля на диагонали — диагональное: оно говорит лишь $∣ x - x ∣ = 0$ . Строгая разделимость — $∣ x - y ∣ = 0 \Rightarrow x = y$ , нулевое расстояние только между совпадающими числами — среди этих четырёх свойств отдельной леммой не стоит. Для рациональной метрики она, конечно, верна; и доказана — но отдельно: лемма qdist_zero_iff в ProcessTopMetric.v устанавливает $∣ x - y ∣ = 0$ тогда и только тогда, когда $x = y$ . К этому различению — между нулём на диагонали и строгой разделимостью — глава вернётся в § 1.3, где оно окажется существенным для абстрактной рамки.

Расстояние позитивно по своей природе

Стоит задержаться на первом из четырёх свойств — неотрицательности. В ToS это не случайная техническая деталь, а проявление сквозного мотива всего тома: расстояние позитивно структурно. Модуль рационального числа неотрицателен не потому, что так удобно постулировать, — а потому, что модуль есть операция, которая по построению отбрасывает знак. <<Отрицательного расстояния>> не бывает не в силу запрета, а в силу того, как расстояние устроено: оно с самого начала есть величина без знака.

Это согласуется с общей позитивной онтологией ToS. Расстояния, нормы, длины, объёмы — все меры разделённости и протяжённости — неотрицательны не по соглашению, а структурно. Глава встретит этот мотив ещё не раз: он вернётся, когда речь пойдёт об интеграле от неотрицательной функции. Метрика — первый его пример в Части V; в E/R/R-разборе (§ 1.3.2) неотрицательность окажется одним из правил (Rules), удерживающих расстояние.

Уровень рациональных чисел

И последнее замечание этого раздела — важное, потому что оно задаёт тон всей главе. Всё, что построено в § 1.2, — qdist и его четыре свойства — работает на уровне рациональных чисел. Это расстояние между двумя $Q$ -числами, не между процессами и не между классами процессов.

Различать уровни придётся постоянно, и глава с самого начала проводит границу. Расстояние на $Q$ — завершённое, рациональное, простое — это фундамент. Но интересный для анализа объект — не рациональное число, а процесс; и расстояние между процессами устроено сложнее, чем $∣ x - y ∣$ . К нему глава перейдёт в § 1.4, построив сначала общую рамку — абстрактное метрическое пространство.

Абстрактное метрическое пространство

Метрическое пространство как система

Расстояние на $Q$ — частный случай. Чтобы говорить о расстоянии вообще — между процессами, между векторами, между чем угодно, — нужна общая рамка: понятие метрического пространства как такового.

Сразу одна оговорка о точности. Абстрактная рамка, которую мы сейчас построим, фиксирует метрическую структуру без общей аксиомы разделимости ( $d (x, y) = 0 \Rightarrow x = y$ ); строго говоря, её честнее называть metric-like, или псевдометрической. Для рациональной метрики разделимость верна и доказывается отдельно (§ 1.3.4); рамка же берёт ровно те гипотезы, которые нужны для общих рассуждений. Глава пользуется привычным словом <<метрическое пространство>> — так названа и сама Rocq-секция, — но строгий читатель пусть держит эту оговорку в виду с самого начала.

В терминах ToS метрическое пространство — это система с характерным набором ролей и правил. Элементы — точки пространства. Роль — расстояние, мера разделённости двух точек. Правила — те самые четыре аксиомы: неотрицательность, нуль на диагонали, симметрия, неравенство треугольника; из них треугольник играет роль конституции, скрепляющей пространство в целое.

Эту рамку мы формализуем параметрически — так, чтобы всё доказанное в ней годилось сразу для всякого конкретного метрического пространства. Средство — Rocq-механизм Section: внутри секции фиксируются носитель (произвольный тип), функция расстояния и четыре гипотезы о ней, а всё, что доказано внутри, автоматически верно для любого носителя и любой функции, этим гипотезам удовлетворяющей. В MetricSpace.v это записано так:

Section MetricSpaces.
 
Variable X : Type.
Variable d : X -> X -> Q.
 
Hypothesis d_nonneg : forall x y, 0 <= d x y.
Hypothesis d_zero : forall x, d x x == 0.
Hypothesis d_sym : forall x y, d x y == d y x.
Hypothesis d_triangle : forall x y z, d x z <= d x y + d y z.

$X$ — произвольный носитель, $d$ — функция расстояния, четыре Hypothesis — те свойства, которым $d$ обязано удовлетворять. Всё, что доказывается внутри секции, доказывается для любого такого $X$ и $d$ . Это и есть общая теория: одна рамка, годная для всякого конкретного метрического пространства.

Заметим методологический выбор. Rocq позволил бы оформить эту рамку и через классы типов; ToS-формализация сознательно берёт Section с явными параметрами. Причина в том, что явная параметричность делает зависимости видимыми: глядя на лемму из секции, сразу видно, от каких именно гипотез о $d$ она зависит, — ничто не спрятано в неявный вывод класса.

Разбор E/R/R: метрика как система

Раз метрическое пространство есть система, к нему приложима методология E/R/R, развёрнутая в Части I: всякая система разбираема на три аспекта — Elements, Roles, Rules. Проведём этот разбор. Он ничего не навязывает пространству извне — он разворачивает ту же разметку, что уже стоит в заголовке опорного файла: элементы — точки; роль — расстояние как мера разделённости; правила — неравенство треугольника (как конституция), симметрия, позитивность.¹ Вести разбор будем в онтологическом порядке — Rules $\to$ Roles $\to$ Elements, — хотя познавательно мы прошли обратным путём: сначала увидели точки, затем расстояние между ними, и лишь потом — аксиомы, которым оно подчинено.

Оговорка о статусе — та же, что при разборе записи Distinction в Части I. Называя метрическое пространство системой, мы ведём содержательную онтологическую интерпретацию; в коде это параметрическая Section с носителем и четырьмя гипотезами, а не объект типа System $L$ с приписанным уровнем иерархии. Разбор читает структуру, а не приписывает файлу нового формального содержания.

Rules — правила, удерживающие пространство (закон $L 5$ : правила стоят над тем, что организуют). Здесь работают два слоя. Универсальный — законы $L 1$ – $L 5$ , общие для всякой системы. Конкретный — четыре аксиомы метрики, специфичные для расстояния: неотрицательность, нуль на диагонали, симметрия и — главное — неравенство треугольника, играющее роль конституции, скрепляющей пространство в связное целое (без него отдельные расстояния не складывались бы в единую меру). Здесь же проходит честная граница, отмеченная в § 1.3.4: строгой разделимости абстрактная Section как общую гипотезу не берёт и потому фиксирует структуру чуть слабее полной метрики. По устройству правил видно и то, как заполняются позиции: носитель дан как параметр, точки не подбираются алгоритмом — Section задаёт потенциал (носитель, расстояние, гипотезы), а конкретные пространства — $Q$ с qdist или векторы QVec с $L^{\infty}$ -расстоянием — его актуализируют.

Roles — значимость позиций (закон $L 4$ : каждая роль структурно обоснована). Роль в этой системе одна и центральная: расстояние $d$ — мера разделённости двух точек, то, зачем точки значимы друг для друга. Эта роль не произвольна: по $L 4$ её достаточным основанием служат сами четыре аксиомы, благодаря которым $d$ есть именно расстояние, а не любая функция двух аргументов. Из роли расстояния разворачиваются качественные позиции, на которых держится весь дальнейший анализ: <<близко>> ( $d < ε$ ) и <<далеко>> ( $d \geq ε$ ), а когда расстояние прикладывается вдоль процесса — <<сходится>> и <<расходится>>.²

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — точки пространства. В рациональной метрике это сами числа $Q$ , конечные как запись; в процессной метрике (§ 1.4) носителями станут процессы, конечные на каждой стадии. По $L 1$ каждая точка тождественна себе — без этого её нельзя было бы устойчиво опознавать в разных сравнениях. А принцип $P 4$ объясняет уже отмеченную особенность типа d : X -> X -> Q: значение расстояния на каждом сравнении есть конечное рациональное число, не элемент завершённого << $R$ >>. Актуализация здесь конечна по самому устройству; <<действительное>> расстояние, если оно понадобится, само окажется процессом (§ 1.4), а не готовым элементом.

Сведём разбор в таблицу.

Компонент	Что фиксирует	E/R/R
носитель $X$ (точки)	что есть в пространстве	Element
$d : X \to X \to Q$	мера разделённости	Role
<<близко>>/<<далеко>>, <<сходится>>/<<расходится>>	ролевые позиции	Role
неотрицательность, нуль, симметрия	удерживают $d$ как расстояние	Rule (конкр.)
неравенство треугольника	конституция	Rule (конкр.)
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: точки суть элементы, расстояние — роль, аксиомы — правила, и ни один компонент не претендует на две категории сразу. Самореференции нет: расстояние работает над точками — по $L 5$ операция стоит уровнем выше своих операндов, — а не применяется к самому себе. По критерию хорошей сформированности, введённому в Части I, метрическое пространство хорошо сформировано.

Разбор не самоцель — он объясняет уже сделанные в главе выборы. Почему расстояние рационально-значно (§ 1.3.3) — потому что элементы актуализуются конечно ( $P 4$ ). Почему разделимость вынесена за пределы аксиом абстрактной рамки (§ 1.3.4) — потому что она принадлежит конкретному слою правил отдельных пространств, не универсальному. Почему именно треугольник назван конституцией — потому что среди правил он один скрепляет разрозненные расстояния в связное целое. И тот же разбор задаёт образец для всей Части V: топологию, непрерывность, производную, интеграл мы будем читать как системы, каждую со своей E/R/R-структурой, разворачивая её из заголовка соответствующего файла.

Расстояние со значением в рациональных

Одна деталь определения существенна и заслуживает отдельного слова. Функция расстояния имеет тип d : X -> X -> Q: расстояние принимает значения в рациональных числах, не в каких-либо <<действительных>>.

На этом уровне формализации ToS выбирает рационально-значную метрику: каждый конечный тест расстояния даёт значение в $Q$ . У выбора есть резон. Завершённого множества действительных чисел под $P 4$ нет; <<действительное>> в ToS само есть процесс. Если бы расстояние принимало значения в << $R$ >>, оно было бы уже не простой мерой, выдающей готовое число, а процессом — со своими представителями, эквивалентностью и доказательством независимости от выбора представителя. Метрики со значениями в процессных действительных вводить можно — это не противоречит $P 4$ , коль скоро такое расстояние само читается процессно, — но они требуют отдельного, более позднего слоя. Абстрактная рамка § 1.3 этот слой не строит: она берёт расстояние рациональным — на каждом сравнении двух точек $d$ выдаёт конкретное рациональное число. А когда расстояние нужно рассмотреть как процесс — это, как будет видно в § 1.4, делается не заменой $Q$ на << $R$ >> в типе $d$ , а тем, что само $d$ применяется вдоль процесса и порождает последовательность рациональных значений.

Метрика или псевдометрика: точная оговорка

Здесь нужна аккуратность, иначе абстрактная рамка прозвучит сильнее, чем она есть. Среди четырёх гипотез секции есть d_zero — но посмотрим на её форму внимательно. d_zero утверждает только: $d (x, x) = 0$ — расстояние от точки до неё самой есть нуль. Это нуль на диагонали.

{ Классическое определение метрики требует большего — строгой разделимости: $d (x, y) = 0 \Rightarrow x = y$ , то есть нулевое расстояние возможно только между совпадающими точками. И вот этой, более сильной гипотезы в абстрактной секции MetricSpace.v нет — она не входит в четвёрку Hypothesis. }

Что это значит? Что абстрактная секция, строго говоря, фиксирует не полную метрику, а структуру чуть более слабую — если держаться строгой терминологии, ближе к псевдометрике. Это не упущение: для многих рассуждений (сходимость, Коши, сжатие) строгая разделимость и не нужна, и секция честно берёт ровно те гипотезы, которые работают. А там, где разделимость требуется, она доказывается отдельно для конкретного пространства. Для рационального расстояния она есть — в ProcessTopMetric.v лемма qdist_zero_iff устанавливает: $∣ x - y ∣ = 0$ тогда и только тогда, когда $x = y$ . То есть рациональная метрика разделимость имеет; абстрактная же рамка её как общую гипотезу не предполагает. Глава отмечает это разведение, чтобы читатель, строго различающий метрику и псевдометрику, не принял абстрактную секцию за большее, чем она утверждает.

Что доказано в общей рамке

{ Внутри этой рамки мы вводим ключевые понятия анализа — те, что дальше понадобятся всей Части V, — и доказываем несколько общих лемм. Понятия три: Коши-последовательность в метрическом пространстве (значения сколь угодно сближаются после некоторого рубежа), предел последовательности и сжимающее отображение. В MetricSpace.v им отвечают is_cauchy_metric, is_limit_metric и is_contraction_metric. }

{ Леммы — общие факты, верные во всяком метрическом пространстве. Неотрицательность с переставленными аргументами (d_nonneg_alt). Если последовательность сходится к двум пределам, расстояние между этими пределами сколь угодно мало (limit_dist_zero) — зародыш единственности предела. Всякая сходящаяся последовательность есть Коши (cauchy_of_limit) — одна из двух классических импликаций между сходимостью и свойством Коши. И несколько лемм о сжимающих отображениях: множитель сжатия неотрицателен, строго меньше единицы, сжатие не увеличивает расстояний. }

Всё это — общая теория, доказанная раз и для всякого метрического пространства. MetricSpace.v несёт восемнадцать проверенных лемм и не использует ни одной аксиомы; из них к абстрактной секции относятся семь, а остальные принадлежат метрике на $Q$ и $L^{\infty}$ -метрике на QVec, о которых речь ниже. На эту общую рамку и обопрутся дальнейшие построения — начиная со следующего раздела, где расстояние впервые станет процессом.

Два процессных расстояния: поточечное и конечногоризонтное{Два процессных расстояния}

Расстояние перестаёт быть числом

Вот онтологический центр главы. В классической математике расстояние между двумя действительными числами $x$ и $y$ — это одно число, $d (x, y) \in R$ , готовое и завершённое. Под $P 4$ завершённого $R$ нет, а сами <<действительные>> суть процессы. Что тогда есть расстояние между двумя процессами?

Ответ предсказуем по всей логике Части IV: расстояние между процессами само есть процесс. Не завершённое число, а разворачивающаяся по уровням уточнения величина. Это согласуется с общей онтологией: всё, что в классике было <<действительным числом>>, в ToS есть процесс, — и расстояние не исключение. В терминах E/R/R-разбора (§ 1.3.2) это значит, что носителями-Elements теперь выступают процессы — конечные на каждой стадии по $P 4$ , — тогда как роль расстояния сохраняется.

Но здесь нужна осторожность, и в ней — всё содержание раздела. В репозитории есть две разные процессные конструкции расстояния, и смешивать их нельзя. Одна — поточечная; другая — усечённая, конечногоризонтная. Разберём обе.

Поточечное расстояние и метрическое Коши

Первая конструкция самая прямая. Даны два процесса $P$ и $Q$ — каждый есть функция из номера шага в рациональное приближение. На каждом шаге $n$ у них есть рациональные значения $P (n)$ и $Q (n)$ , и между этими рациональными значениями есть расстояние — то самое $∣ P (n) - Q (n) ∣$ . Собрав эти расстояния по всем шагам, получаем процесс:

n ⟼ ∣ P (n) - Q (n) ∣.

Это поточечное расстояние — процесс, дающий на каждом уровне рациональное расхождение приближений. Сам объект — процесс, а не его <<предельное значение>>.

Оговорим точно статус этого определения в коде. Готового имени rp_dist для функции $n \mapsto ∣ P (n) - Q (n) ∣$ в опорных файлах главы нет — глава вводит это поточечное расстояние как понятие. Зато в ProcessTopMetric.v есть тесно связанная и для анализа более важная конструкция — метрическое условие Коши:

Definition metric_cauchy (a : RealProcess) : Prop :=
  forall eps, 0 < eps ->
    exists N, forall m n, (N <= m)%nat -> (N <= n)%nat ->
      qdist (a m) (a n) < eps.

{

Процесс $a$ удовлетворяет metric_cauchy, если его значения, измеряемые рациональным расстоянием qdist, сколь угодно сближаются после некоторого рубежа. И ProcessTopMetric.v доказывает, что это в точности обычное процессное условие Коши: }

Theorem metric_cauchy_equiv : forall a,
  is_Cauchy a <-> metric_cauchy a.

metric_cauchy_equiv — мост между двумя формулировками: <<быть Коши>> в смысле Главы 4.2 и <<быть Коши>> в метрических терминах через qdist — одно и то же. Это лучший якорь для тезиса <<метрика как процесс>>: рациональное расстояние qdist прикладывается вдоль процесса, и метрический язык в точности ложится на уже построенный аппарат Коши.

И ещё одна оговорка — по поводу естественного ожидания. Хочется сказать: если $P$ и $Q$ — оба процессы Коши, то и поточечный процесс расстояний $n \mapsto ∣ P (n) - Q (n) ∣$ есть Коши. Содержательно это верно, и доказывается коротко — неравенством треугольника для рационального модуля:

∣ P_{m} - Q_{m} ∣ - ∣ P_{n} - Q_{n} ∣ \leq ∣ P_{m} - P_{n} ∣ + ∣ Q_{m} - Q_{n} ∣,

так что если правые части малы (а они малы, раз $P$ и $Q$ — Коши), мало и левое расхождение. Лемма именно такого вида — <<процесс расстояний двух Коши-процессов есть Коши>> — теперь доказана: это cauchy_abs_is_cauchy из файла RealPointMetric.v. В семи опорных файлах этой главы её не было, но в репозитории она есть; так что приводимое здесь — уже не только доказательный набросок: оценка закреплена отдельной теоремой, и § 1.8.2 покажет, что вместе с согласованностью она и даёт метрику на классах.

Конечногоризонтная наблюдаемая дистанция

Вторая конструкция — иная, и путать её с первой нельзя. Она задана в ProcessSpace.v и называется process_dist:

Fixpoint process_dist_aux (f g : RealProcess) (n : nat) : Q :=
  match n with
  | O => Qabs (f 0%nat - g 0%nat)
  | S n' => process_dist_aux f g n' + Qpow (1#2) n * Qabs (f n - g n)
  end.
 
Definition process_dist (f g : RealProcess) (N : nat) : Q :=
  process_dist_aux f g N.

Прочтём внимательно. process_dist $f g N$ при фиксированном $N$ — это конечная взвешенная сумма: по всем шагам от $0$ до $N$ берутся расхождения $∣ f (k) - g (k) ∣$ , каждое с весом $(1/2)^{k}$ , и складываются. У результата есть аргумент $N$ — горизонт, — и от него сумма зависит.

Назовём эту конструкцию точно: process_dist — это конечногоризонтная наблюдаемая дистанция. Расстояние между двумя процессами, увиденное до уровня $N$ — до конечного горизонта наблюдения. Чем дальше отодвинут горизонт $N$ , тем больше шагов учтено; но при всяком фиксированном $N$ это конечная рациональная величина.

Существенно, чем process_dist не является. Это не поточечный процесс расстояний $n \mapsto ∣ P (n) - Q (n) ∣$ из предыдущего пункта — там на каждом шаге одно расхождение, здесь до каждого горизонта $N$ накопленная взвешенная сумма всех расхождений. (Если же $f$ и $g$ зафиксировать, а $N$ пустить пробегать номера шагов, то само отображение $N \mapsto ‘ p r oces s_{d} i s t ‘ f g N$ есть процесс — процесс накопленных конечногоризонтных расстояний; это иной процесс, чем поточечный $n \mapsto ∣ P (n) - Q (n) ∣$ , и путать их нельзя.) И process_dist — не предельное расстояние между классами процессов: никакого перехода к пределу в определении нет, есть конечный горизонт. process_dist — удобная мера того, насколько два процесса разошлись в пределах обозримого; весовой множитель $(1/2)^{k}$ гарантирует, что дальние шаги вносят всё меньший вклад.

Сведём три конструкции расстояния на процессах в таблицу — она закрепляет различение, на котором держится весь раздел:

Конструкция	Тип	Что измеряет
$n \mapsto	P(n)-Q(n)	$
`process_dist` $P QN$	$Q$ , при фиксированном $N$	взвешенная сумма расхождений до горизонта $N$
$N \mapsto ‘ p r oces s_{d} i s t ‘ P QN$	процесс над $Q$	накопленные конечногоризонтные расстояния

{

Первая строка — поточечное расстояние § 1.4.2; вторая — сама process_dist из ProcessSpace.v, рациональное число при заданном горизонте; третья — та же process_dist, прочитанная как процесс по горизонту. Все три законны; смешивать их нельзя. }

ProcessSpace.v как инфраструктурный слой

{ Вокруг process_dist естественно построить небольшой топологический аппарат — и он построен: cylinder (совпадение процессов на первых $N$ координатах в пределах радиуса), process_ball (шар по конечногоризонтной дистанции), process_bounded (ограниченность процесса). Доказаны базовые факты — расстояние процесса до самого себя есть нуль, центр лежит в своём шаре, постоянный процесс ограничен. Всё это собрано в файле ProcessSpace.v. }

Здесь важно точно очертить, что этот слой есть, а что — нет. ProcessSpace.v — слой инфраструктурный: он закладывает заготовки топологии на пространстве процессов, но полной метрики на типе классов RealPoint не строит. Есть в нём теорема с громким именем — process_space_complete, — и тут глава обязана назвать вещи своими именами. Вопреки имени, process_space_complete не есть теорема о полноте пространства процессов. Если вчитаться в её доказательство, она оказывается простой конъюнкцией двух уже доказанных тривиальных лемм: <<расстояние процесса до себя есть нуль>> и <<центр лежит в своём шаре>>. Это полезная сводка двух элементарных фактов — но не утверждение о том, что всякая Коши-последовательность процессов сходится. Имя обещает больше, чем теорема даёт; и наш аудит это прямо отмечает. О настоящей полноте — и о том, почему она здесь понятие, а не доказанная теорема, — речь пойдёт в § 1.6.

Метрика над процессами и общая схема

Универсальный тип процесса

До сих пор процессы были процессами Коши над $Q$ — функциями из номера шага в рациональное приближение. Но понятие процесса шире, и его стоит формализовать в самом общем виде: процесс над произвольным типом $A$ — это просто функция из номеров шагов в $A$ , пошагово индексированное вычисление, выдающее на каждом шаге значение типа $A$ . В ProcessGeneral.v это записано так:

Definition GenProcess (A : Type) := nat -> A.

Процесс Коши — частный случай, $A = Q$ . Бинарный процесс из Главы 4.5 — частный случай, $A = ‘ b oo l ‘$ . GenProcess — общая форма их всех.

Над этим общим типом мы строим и общий аппарат: observe (прочесть значение на шаге $n$ ), prefix (собрать первые $n$ значений в список — конечное наблюдение, в духе $P 4$ ), process_map (применить функцию к каждому шагу), const_process (постоянный процесс). Всё это — содержание ProcessGeneral.v.

Обобщённое условие Коши

Главное, что даёт общая схема, — обобщённое условие Коши. Над любым типом $A$ , снабжённым функцией расстояния $dist : A \to A \to Q$ , можно спросить, стабилизируется ли процесс:

Definition is_cauchy_gen {A : Type} (dist : A -> A -> Q)
                         (p : GenProcess A) : Prop :=
  forall eps : Q, 0 < eps ->
    exists N : nat, forall m n : nat,
      (N <= m)%nat -> (N <= n)%nat -> dist (p m) (p n) < eps.

Заметим: расстояние $dist$ здесь снова со значением в $Q$ — та же логика, что и в абстрактной метрической рамке § 1.3. is_cauchy_gen обобщает условие Коши из Главы 4.2 на любой тип с рациональным расстоянием. И стоит убедиться, что обобщение не разошлось с исходным понятием: для $A = Q$ с расстоянием $∣ x - y ∣$ обобщённое условие в точности совпадает с обычным Коши. Это совпадение и подтверждает лемма cauchy_Q_equiv из ProcessGeneral.v — is_cauchy и is_cauchy_gen Qdist эквивалентны. По разбору § 1.3.2 это та же роль — расстояние как мера разделённости, — обобщённая на произвольный тип-носитель $A$ : меняются Elements, сама роль расстояния остаётся.

{ Полезная лемма этого слоя — process_map_cauchy: отображение, не увеличивающее расстояний, переводит Коши-процесс в Коши-процесс. И родственная ей, уже в ProcessTopMetric.v, — cauchy_map_lipschitz: Липшицево отображение сохраняет свойство Коши. Эти леммы — задел для непрерывности: они говорят, что <<хорошие>> отображения уважают сходимость. К непрерывности глава вернётся в § 5.3 тома. }

Имя process_equiv в разных файлах

Здесь нужна оговорка об именах — маленькая, но важная, потому что без неё легко запутаться. Имя process_equiv встречается в репозитории не в одном смысле.

В ProcessGeneral.v process_equiv — это обобщённое поточечное отношение: два процесса эквивалентны, если согласованы на каждом шаге относительно заданного отношения $eq_{A}$ на $A$ . В ProcessCore.v имя process_equiv носит другое отношение — одинакового предела для рациональных процессов: два процесса Коши эквивалентны, если сходятся к одному числу (это отношение Главы 4.3, по которому строилась точка как класс). А в CauchyReal.v родственное отношение одинакового предела названо cauchy_equiv.

Это разные отношения, и совпадение имён — лишь совпадение имён. Глава пользуется каждым в его локальном смысле и, упоминая process_equiv, всякий раз имеет в виду то отношение, которое определено в обсуждаемом файле. Поточечное согласие (ProcessGeneral.v) и одинаковый предел (ProcessCore.v) — не одно и то же, и эту границу глава держит.

Мост между типами процессов

Часть V постоянно ходит между двумя типами: CauchySeq из CauchyReal.v — запись, объединяющая последовательность с доказательством её Коши-свойства, — и RealProcess из ProcessCore.v — голый процесс nat -> Q. Один тип удобен, когда Коши-свойство нужно нести при себе; другой — когда процесс рассматривается как чистое вычисление.

Чтобы две линии не оставались несообщающимися ветвями, между этими типами нужно навести мост — переходы туда и обратно, при которых сохраняются Коши-свойство и эквивалентность. Этот мост и построен в файле ProcessBridge.v: связка техническая, но необходимая — без неё линия CauchyReal и линия ProcessCore развивались бы порознь. Ещё один пролёт к тому же мосту добавляет ProcessGeneral.v — лемма cauchy_seq_is_gen_process: всякая CauchySeq есть, в частности, GenProcess над $Q$ , удовлетворяющий обобщённому условию Коши. Так три уровня — CauchySeq, RealProcess, общий GenProcess — оказываются сшиты в одну согласованную картину, по которой дальнейшие главы Части V будут свободно перемещаться.

Полнота: понятие и граница

Жирная черта

Этот раздел — самый осторожный в главе, и начать его надо с прямого тезиса, набранного без обиняков.

Полнота в этой главе вводится как понятие, а не доказывается как свойство конкретного пространства.

Сказать это нужно сразу, потому что здесь проходит та граница, за которой осторожный план Части V отделяется от соблазнительного, но неверного заявления <<процессный анализ полон>>. Глава 5.1 строит определение полноты и честно показывает, где оно пока остаётся определением, не превращённым в теорему.

Определение полноты

Начнём с того, что значит для метрического пространства быть полным. Свойство это — <<без дыр>>: процесс, чьи значения сближаются, непременно к чему-то сходится, и это <<что-то>> есть точка самого пространства. Иначе говоря, пространство полно, если всякая Коши-последовательность его точек имеет предел. В абстрактной секции MetricSpace.v мы записываем это так:

Definition is_complete_metric : Prop :=
  forall f : nat -> X, is_cauchy_metric f -> exists l : X, is_limit_metric f l.

И здесь ключевое слово — Definition. is_complete_metric — это определение, предикат: формулировка свойства <<быть полным>>. Само по себе оно ничего не утверждает о каком-либо конкретном пространстве. Оно говорит, что значит быть полным, — но не говорит, что хоть одно пространство этим свойством обладает.

Чего в опорных файлах нет

Теперь — честная инвентаризация. В семи опорных файлах Главы 5.1 нет теоремы, которая доказывала бы полноту. Нет утверждения << $Q$ полно>> (и быть не может — $Q$ как раз неполно: процесс рациональных приближений к иррациональному числу есть Коши, но рационального предела не имеет). Нет утверждения <<CauchyReal полно>>. Нет утверждения <<пространство процессов полно>>. Понятие is_complete_metric введено — но ни к одному пространству как доказанная теорема не применено.

Это не пробел и не недоработка. Это честная граница: полнота конкретного процессного пространства — содержательная задача формализации, и Глава 5.1 её не закрывает. Она вводит понятие, а доказательство полноты для того или иного пространства оставляет как направление дальнейшей работы.

Стоит уточнить, что именно про CauchyReal доказано. Файл CauchyReal.v содержит лемму cauchy_complete_ self и родственные ей — свойства самих Коши-представителей: скажем, что процесс рациональных приближений согласуется сам с собой в подходящем смысле. Это полезные базовые факты. Но это не полная метрическая полнота фактор-пространства классов: лемма о свойстве представителя и теорема о том, что всякая Коши-последовательность классов имеет предел, — утверждения разного масштаба, и второго в опорных файлах нет.

И — по уже сказанному в § 1.4 — process_space_complete из ProcessSpace.v, вопреки громкому имени, полноты не доказывает: это конъюнкция двух тривиальных лемм. Имя содержит слово <>; теорема за ним — нет.

Доказательство Коши и вычислимый модуль

Есть соблазнительный довод, который здесь надо разобрать аккуратно, потому что в нём есть и верное зерно, и опасное преувеличение. Довод такой: классическое доказательство полноты метрического пространства обыкновенно опирается на аксиому зависимого выбора — надо для каждого уровня точности выбрать подходящий номер; а в ToS, мол, выбор не нужен, потому что процесс Коши <<уже несёт>> модуль сходимости.

Зерно истины тут есть. Тип CauchySeq объединяет последовательность с доказательством её Коши-свойства; и в конструктивном чтении доказательство Коши действительно указывает на правило — на способ по точности назвать рубеж.

Но преувеличение тоже рядом, и его надо назвать. CauchySeq хранит доказательство Коши-свойства в Prop — в мире логических утверждений. Этого достаточно для логической формализации свойства Коши. Но из этого автоматически не следует, что из такого доказательства можно вычислительно извлечь модуль сходимости как данные — как функцию <<по $ε$ дать $N$ >>, которую можно запустить и получить число. Извлечение модуля как вычислимого объекта требует информативного варианта свойства — например, регулярного Коши-условия (is_Regular_ Cauchy из ProcessCore.v) или явно приложенного модуля. ToS не случайно различает is_Cauchy и is_Regular_ Cauchy: это различие как раз и отделяет логическое свойство от несущего вычислимые данные.

Поэтому глава формулирует осторожно. Не <<доказательство Коши уже есть алгоритм>> — а так: в ToS-чтении доказательство Коши указывает на правило нахождения рубежа; а для вычислимой реализации этого правила полезен явный модуль или регулярный вариант Коши-свойства. Онтологический тезис о том, что в ToS существование и построимость сближаются, остаётся в силе как сквозной процессный мотив ToS и как интерпретация — но он не есть автоматическое свойство всякого Prop-доказательства, и глава не выдаёт его за таковое.

Что остаётся

{ Подведём черту под разделом. Полнота в Главе 5.1 — понятие: определение is_complete_metric, чистое и проверяемое. Применение этого понятия к конкретному процессному пространству — доказательство, что то или иное пространство классов полно, — в опорных файлах главы не проведено и честно оставлено направлением. Это и есть <<режим инфраструктуры>>, о котором предупреждал § 1.1: понятие построено, граница названа, и одно от другого не выдаётся. }

Архимедовость как топливо

Зачем метрике архимедовость

Метрика построена — но чтобы она работала в анализе, нужно ещё одно свойство, без которого $ε$ -рассуждения повисли бы в воздухе. Это архимедовость.

Почти всякое аналитическое рассуждение имеет вид: <<задайте точность $ε$ — и найдётся уровень $N$ , начиная с которого расхождение меньше $ε$ >>. Чтобы такой ход был осмыслен, нужно, чтобы для всякого, сколь угодно малого $ε$ этот $N$ существовал. Иначе говоря, нужно, чтобы дробление точности рано или поздно пробивало любой заданный порог. Это и есть архимедовость — свойство, унаследованное процессной метрикой от рациональных чисел $Q$ (Глава 3.4 тома).

Конкретно для метрики важна такая её форма: для любого $ε > 0$ существует натуральное $N$ , при котором $(1/2)^{N} < ε$ . Половинное дробление — $1, 1/2, 1/4, 1/8, \dots$ — рано или поздно опускается ниже всякого порога.

Архимедовость делает алгоритмы конечными

У этого свойства есть не только онтологический смысл — <<точность достижима>>, — но и прямой вычислительный. Архимедовость делает аналитические алгоритмы конечными.

Рассмотрим типичный $ε$ -алгоритм: половинное деление интервала. На каждом шаге ширина текущего интервала уменьшается вдвое; работа идёт, пока ширина не станет меньше требуемого $ε$ . Вопрос: остановится ли этот цикл? Ответ даёт архимедовость: раз найдётся $N$ с $(1/2)^{N} < ε$ , то после $N$ шагов ширина заведомо мала, и цикл завершится не более чем за $N$ итераций. Архимедовость поставляет циклу верхнюю границу числа шагов — и для конкретного рационального $ε$ это $N$ находится явным перебором степеней двойки. Стоит, впрочем, держать различие: формальная теорема существования такого $N$ и исполняемая процедура его поиска — близкие, но технически разные слои; если нужен именно запускаемый алгоритм, его задают отдельно.

В этом — связь онтологии с вычислением. То, что онтологически конечно (процесс, у которого точность достижима), оказывается и алгоритмически конечно (вычисление, которое завершается за обозримое число шагов). Архимедовость — мост между двумя конечностями.

Вычислительный пример: сколько шагов довольно

Здесь — обещанный третий слой изложения. Сделаем архимедовость осязаемой: посчитаем, сколько шагов половинного дробления довольно для нескольких конкретных уровней точности.

Задача: для данного $ε$ найти наименьшее $N$ , при котором $(1/2)^{N} < ε$ . Это $N$ вычислимо — его прямо находят перебором степеней двойки. Вот результат для трёх типичных порогов:

Требуемая точность $ε$	Достаточное $N$	Проверка
$1/10$	$4$	$(1/2)^{4} = 1/16 < 1/10$
$1/100$	$7$	$(1/2)^{7} = 1/128 < 1/100$
$1/1000$	$10$	$(1/2)^{10} = 1/1024 < 1/1000$

Прочтём таблицу. Чтобы расхождение упало ниже одной десятой, довольно четырёх шагов дробления: $1/16$ уже меньше $1/10$ . Ниже одной сотой — семи шагов: $1/128 < 1/100$ . Ниже одной тысячной — десяти: $1/1024 < 1/1000$ . Числа в среднем столбце не угаданы — они вычислены, и каждую строку можно проверить прямым сравнением дробей, что и сделано в правом столбце.

Это и есть архимедовость в работе. Не философский тезис <<точность когда-нибудь достигнется>>, а конкретная таблица: вот сколько шагов довольно. Читатель видит, что $ε$ достигается за конечное, заранее вычислимое число шагов — и видит, что с уменьшением $ε$ в десять раз нужное $N$ растёт всего на три-четыре шага. $ε$ -рассуждения процессного анализа стоят на этой вычислимой почве.

Оговорка о статусе аксиом

И — честная оговорка, в духе всей главы. Семь основных опорных файлов Главы 5.1 в своих шапках заявляют статус <<0 axioms>> — ни одной аксиомы; об этом сказано в § 1.1. Для строгого аудита конкретной теоремы статус всё равно проверяется командой Print Assumptions — заявление в шапке файла его не заменяет.

{ Настоящий раздел, однако, опирается дополнительно на отдельный файл — Archimedean_ERR.v, где архимедовость $Q$ и формализована. Поэтому глава не делает огульного заявления <<вся глава стоит на нуле аксиом>>. Точная формулировка такая: семь основных файлов — без аксиом; раздел об архимедовости привлекает Archimedean_ERR.v дополнительно, и его зависимость от аксиом, если она есть, следует устанавливать отдельно — командой Print Assumptions для соответствующей теоремы. Это та же дисциплина, что и в Главе 4.6: статус аксиом проверяется по конкретной теореме, а не приписывается файлу или главе оптом. }

Что построено и что готовится. Итог главы

Итог в трёх столбцах

Глава открывала Часть V, и честнее всего подвести её итог так, как требует <<режим инфраструктуры>>: тремя списками — что построено, что не построено, что готовится дальше. Без смешения одного с другим.

Построено и проверено.

Рациональная метрика на $Q$ : расстояние $∣ x - y ∣$ и четыре аксиомы метрики, все доказанные (одна конструкция под тремя именами — Q_dist, qdist, Qdist).
Абстрактная метрическая рамка: метрическое пространство как параметрическая Section, с понятиями Коши, предела, сжатия и общими леммами — без аксиом (в файле зафиксировано восемнадцать проверенных результатов, включая слои $Q$ и QVec).
Процессное условие Коши через рациональное расстояние — metric_cauchy, доказанно эквивалентное обычному is_Cauchy (теорема metric_cauchy_equiv).
Конечногоризонтная наблюдаемая дистанция на пространстве процессов — process_dist, взвешенная сумма расхождений до уровня $N$ .
Мосты между типами процессов: CauchySeq, RealProcess и общий GenProcess сшиты в одну согласованную картину (ProcessBridge.v, cauchy_seq_is_gen_process).

Не построено в этой главе.

Фактор-тип RealPoint как Rocq-объект здесь не строится — глава работала с процессами и рациональными расстояниями.
Метрика на классах RealPoint как отдельная Rocq-структура в этой главе не вводится — но в репозитории она построена (файл RealPointMetric.v: rp_dist с аксиомами метрики и rp_dist_Proper — независимостью от выбора представителя); см. § 1.8.2.
Полная метрическая полнота пространства этих классов — не доказана; полнота введена как понятие (§ 1.6), не как теорема о конкретном пространстве.

Готовит дальше.

Открытые шары $B (P, ε)$ и понятие <<близких процессов>> — материал § 5.2, топологии.
Непрерывность как сохранение близости — материал § 5.3; заделом служат леммы cauchy_map_lipschitz и process_map_cauchy этой главы.

Метрика на классах: построена

{ Список <<не построено>> относится к этой главе и её семи опорным файлам. Сама же метрика на классах RealPoint в репозитории построена — отдельным файлом RealPointMetric.v; стоит назвать конкретно, чем именно, чтобы граница главы была очерчена точно.

Во-первых, поточечное расстояние как именованная конструкция — причём сразу со значениями в вещественных, а не рациональных: расстояние двух точек само есть точка (процесс),

‘ r p_{d} i s t ‘ (ab : ‘ R e a l P o in t ‘) := ‘ c a u c h y_{a} b s ‘ (‘ c a u c h y_{s} u b ‘ a b),

то есть $∣ a - b ∣$ как процесс. Во-вторых — те самые две леммы. Первая: процесс расстояний есть Коши (cauchy_abs_is_cauchy — та оценка-набросок из § 1.4.2, ставшая теоремой). Вторая: rp_dist согласовано с эквивалентностью — замена представителей на эквивалентные не меняет расстояния (rp_dist_compat и инстанс rp_dist_Proper). Именно вторая лемма спускает расстояние с процессов на классы и превращает RealPoint в метрическое пространство. Сверх того, доказаны и четыре аксиомы метрики — неотрицательность (rp_dist_nonneg), нуль на диагонали (rp_dist_self_zero), симметрия (rp_dist_sym), треугольник (rp_dist_triangle) — и сверх них разделимость (rp_dist_eq_zero_iff). Так что от метрики на классах главу отделяет уже не пробел: она построена, хотя и не в семи файлах этой главы, а в RealPointMetric.v. Открытым остаётся лишь следующий слой — метрическая полнота пространства классов (§ 1.6). }

Мост к многомерному анализу

Одно замечание на будущее. Файл MetricSpace.v содержит не только расстояние на $Q$ , но и $L^{\infty}$ -метрику на рациональных векторах QVec — расстояние, равное наибольшему из покоординатных расхождений (list_max_dist), с доказанными для него четырьмя свойствами метрики. В настоящей главе этот материал не разворачивается — глава осталась в одномерном расстоянии. Но стоит отметить его как мост: процессная метрика не привязана к одному измерению, и когда том дойдёт до многомерного анализа и оптимизации, $L^{\infty}$ -расстояние на QVec окажется готовой отправной точкой.

Итог главы

Глава 5.1 заложила первый аналитический слой Части V — расстояние. Она прошла путь от простейшего рационального $∣ x - y ∣$ через абстрактную метрическую рамку к процессным расстояниям — и на каждом шаге держала границу между тем, что доказано, и тем, что лишь намечено. Главный поворот — поточечное расстояние между процессами само есть процесс, не завершённое число (а наряду с ним process_dist даёт конечногоризонтную дистанцию — иной слой); главная осторожность — полнота есть пока понятие, не теорема. На этом фундаменте Часть V будет строить топологию, непрерывность и весь дальнейший анализ.

{Итог главы — в трёх частях. Первое: что построено. Расстояние между рациональными числами — $∣ x - y ∣$ с четырьмя доказанными аксиомами метрики; абстрактная метрическая рамка как параметрическая Section; расстояние как процесс — metric_cauchy над RealProcess, эквивалентное обычному условию Коши; конечногоризонтная наблюдаемая дистанция process_dist; мосты между CauchySeq, RealProcess и GenProcess. Все семь опорных файлов — без аксиом.}

{Второе: на чём это стоит. Расстояние принимает значения в рациональных числах — завершённого << $R$ >> процессная метрика не требует. Абстрактная секция фиксирует базовую структуру — неотрицательность, нуль на диагонали, симметрию, треугольник; строгая разделимость в неё как общая гипотеза не входит, для рациональной метрики она доказана отдельно. $ε$ -рассуждения опираются на архимедовость $Q$ , которая делает дробление точности вычислимо конечным.}

{Третье: что остаётся открытым. Метрика на классах RealPoint уже построена — вне семи файлов этой главы, в RealPointMetric.v (rp_dist с аксиомами и rp_dist_Proper; § 1.8.2). Открытыми остаются полная метрическая полнота пространства этих классов (полнота введена как понятие, не как доказанная теорема) и реифицированный фактор-тип отдельным объектом — последний ToS не строит сознательно, по $P 4$ (Глава 4.3). Глава дала фундамент — расстояние; топология и непрерывность, что встанут на нём, — предмет следующих глав Части V.}

Часть: Часть V. Топология и анализ процессов · Том: «Математика»

Понятия: Логика · Формализация

Навигация: ← Глава 6. P4 как фильтр — Часть IV · Глава 2. Топология и компактность →

Это дословная E/R/R-разметка в шапке файла MetricSpace.v; здесь она лишь разворачивается по образцу Части I. ↩
Эти четыре позиции — close / far / convergent / divergent — перечислены в строке Status шапки MetricSpace.v. ↩

Путь Мудрости

Проводник