Глава 2. RealProcess как тип

От принципа к типу

Что оставила Глава 4.1

Предыдущая глава довела до полной ясности принцип $P 4$ — принцип конечной актуальности: всякая система в любой момент конечна, а бесконечность есть свойство процесса, а не объекта. Глава показала, откуда $P 4$ берётся, что он делает излишним в стандартной математике и с чем несовместим, и закончила тезисом: действительное число не может быть исходно готовой точкой — исходно оно есть процесс, разворачивающаяся по правилу последовательность рациональных приближений.

Но назвать процесс и построить его как полноценный объект формализации — разные вещи. Глава 4.1 назвала; настоящая глава строит. Её задача — дать процессу определение типа: такого же определённого предмета Rocq-формализации, как индуктивный тип натуральных чисел или тип рациональных. Пока этого определения нет, все разговоры о <<процессном действительном числе>> остаются обещанием; Глава 4.2 обещание выполняет.

Почему именно тип функций

Глава 4.1 уже обмолвилась, каким будет это определение: процесс есть функция из натуральных чисел в рациональные. Прежде чем разворачивать конструкцию во всей строгости, стоит понять, почему тип устроен именно так и почему он в этом устройстве не произволен.

Процессу нужно отвечать на один-единственный род запроса: <<каково приближение на шаге $n$ ?>>. Запрос задаётся натуральным числом — номером шага; ответом служит рациональное число — приближение. Объект, который на всякий вход-номер даёт выход-приближение, есть функция из номеров в приближения. Натуральные числа ToS уже имеет — это индуктивный тип, схема счёта из Части II; рациональные числа ToS уже имеет — это конечные записи, дроби из Части III. Процесс не требует никакого нового исходного материала: он есть функция между двумя уже построенными типами.

Это и делает выбор типа неизбежным, а не произвольным. Можно было бы вообразить процесс как-то иначе — как бесконечный список, как поток, как пару из правила и состояния. Но всякое такое представление либо сводится к функции <<номер шага $\mapsto$ приближение>>, либо протаскивает завершённую бесконечность (бесконечный список как готовый объект), которую $P 4$ как раз и запрещает. Функция из номеров в приближения — наименьшее, чего достаточно, и наибольшее, что $P 4$ позволяет. Тип процесса вычитывается из принципа, а не назначается рядом с ним.

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

Дальнейшее строит этот тип по шагам и разбирает его аппарат. Сперва — голый процесс как тип функций и наблюдение его по конечным префиксам (§ 2.2). Затем — условие, отбирающее из всех процессов те, что годятся в действительные числа: свойство Коши (§ 2.3). Затем — арифметика процессов и теоремы о том, что она не выводит за пределы отобранного класса (§ 2.4). Затем — собственно тип действительного числа, в котором носитель и доказательство сведены вместе, и честный разбор того, что Rocq-формализация ToS даёт этот тип не одним, а несколькими родственными оформлениями (§ 2.5). Затем — отношение, по которому разные процессы задают одно и то же число (§ 2.6), и структурные признаки сходимости (§ 2.7). Наконец — итог и мост к Главе 4.3 (§ 2.8).

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

Голый процесс как тип функций

Определение `RealProcess`{RealProcess}

В Rocq-репозитории ToS базовый процессный тип определён в файле ProcessCore.v и носит имя RealProcess.¹ Определение предельно коротко:

Definition RealProcess := nat -> Q.

Процесс есть функция из натуральных чисел в рациональные. Терм типа RealProcess — это правило, которое всякому номеру шага $n$ сопоставляет рациональное приближение. Ничего сверх этого в определении нет: ни условия сходимости, ни предела, ни структуры — голая функция.

Назовём такой объект голым процессом — голым в том смысле, что на него ещё не наложено никаких условий. Голый процесс может вести себя как угодно: приближаться к некоторому значению, колебаться без предела, разбегаться. Тип RealProcess вмещает их все. Это важно осознать сразу: RealProcess шире класса действительных чисел. Не всякий голый процесс есть число; какие именно процессы числами являются, установит § 2.3. Пока же RealProcess — это общий тип-носитель, пространство, внутри которого числа предстоит ещё выделить.

Простейший обитатель этого пространства — постоянный процесс:

Definition const_process (q : Q) : RealProcess := fun _ => q.

Он на всяком шаге выдаёт одно и то же рациональное число $q$ . Это процесс, который <<уже пришёл>>: его приближения не уточняются, потому что уточнять нечего. Постоянный процесс будет служить пробным камнем во всех дальнейших построениях — простейший случай, на котором проверяется всякое определение.

`RealProcess`{RealProcess} есть тип тотальных функций

Глава 4.1 в § 1.8 уже сделала оговорку, которую здесь нужно развернуть. Технически nat -> Q есть в Rocq тип тотальных функций: терм этого типа определён на всяком $n$ , а не только на тех номерах, что уже были запрошены. Было бы неточно сказать, что в RealProcess <<нет ничего завершённого>>.

Различение здесь такое же, как проведённое в § 1.4 для типа nat. Формально тип RealProcess существует, и терм этого типа есть законный объект Rocq, по которому можно квантифицировать. ToS этого формального факта не отрицает. ToS читает терм типа RealProcess операционально — как правило, которое по предъявленному номеру $n$ вычисляет рациональный ответ. При таком чтении процесс есть схема, разворачивающаяся по запросу, а не собранная воедино бесконечная таблица значений. Завершённой бесконечности как сет-теоретического объекта — готового бесконечного множества пар <<номер, значение>> — в этом чтении нет; но в формальном языке Rocq RealProcess есть именно функциональный тип. Глава держит оба уровня: формальный (функциональный тип) и онтологический (операциональное правило), — и не подменяет один другим.

Стоит отметить и техническую сторону. В Rocq запись nat -> Q есть функциональный тип, построенный поверх двух уже имеющихся типов — nat и Q, — и берущий их как область и кообласть. Определение RealProcess не создаёт ни натуральные, ни рациональные числа заново; оно их использует. Это согласуется с онтологической деривацией § 2.1.2 — процесс не требует нового исходного материала, — но важно видеть, где проходит граница: онтологическая деривация объясняет, почему тип таков, а формально nat и Q — готовые типы языка Rocq, построенные в предыдущих частях тома, и глава 4.2 их не переобосновывает, а применяет.

Наблюдение процесса: префиксы

Если процесс читается операционально — как правило, отвечающее на запросы, — то естественно спросить: что мы реально наблюдаем, имея процесс на руках? Ответ Rocq-формализация даёт в файле ProcessGeneral.v, и ответ этот — конечные префиксы.² Файл вводит универсальный процессный тип GenProcess A := nat -> A — процесс над любым типом $A$ , для $A = Q$ совпадающий по существу с RealProcess, — и две операции наблюдения:

Definition observe {A : Type} (p : GenProcess A) (n : nat) : A := p n.
 
Fixpoint prefix {A : Type} (p : GenProcess A) (n : nat) : list A :=
  match n with
  | O => []
  | S k => prefix p k ++ [p k]
  end.

Операция observe читает значение на одном шаге. Операция prefix собирает первые $n$ значений процесса в конечный список. И вот это — prefix — есть $P 4$ в действии, записанный как функция. Что бы мы ни взяли у процесса, мы берём конечный префикс: список длины $n$ , собранный за $n$ шагов. Файл это и доказывает: лемма prefix_length устанавливает, что префикс длины $n$ имеет ровно $n$ элементов, а лемма prefix_nth — что $k$ -й элемент префикса есть в точности $p (k)$ . Процесс никогда не предъявляется весь; он предъявляется префиксами, и всякий префикс конечен. Это и есть конечная актуальность § 1.1, ставшая операцией: в любой момент наблюдения налицо конечный список, а бесконечен лишь незавершённый процесс их порождения.

Условие Коши: отбор чисел из процессов

Зачем нужен отбор

Тип RealProcess вмещает все голые процессы — и сходящиеся, и расходящиеся, и колеблющиеся без предела. Если действительное число есть процесс, то которым из них? Ясно, что не всяким. Процесс, выдающий $0, 1, 0, 1, 0, 1, \dots$ , не приближается ни к чему: он вечно мечется между двумя значениями. Назвать его действительным числом нельзя — он не уточняет никакого числа, он просто перечисляет два. Чтобы процесс задавал число, его приближения должны сходиться — со временем становиться всё ближе друг к другу.

Значит, тип RealProcess надо сузить. Действительное число — не любой голый процесс, а процесс, прошедший отбор: удовлетворяющий условию сходимости. Это условие ToS, следуя классической традиции и операциональному духу Главы III.4, формулирует как свойство Коши.

Определение свойства Коши

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

Rocq-формализация записывает это так. Процесс есть Коши, если для всякой положительной точности $ε$ можно указать такой номер шага $N$ , что любые два приближения с номерами не меньше $N$ отстоят друг от друга меньше чем на $ε$ . В файле CauchyReal.v (о нём подробно § 2.5) это предикат is_cauchy:

Definition is_cauchy (a : nat -> Q) : Prop :=
  forall eps : Q, 0 < eps ->
    exists N : nat, forall m n : nat,
      (N <= m)%nat -> (N <= n)%nat -> Qabs (a m - a n) < eps.

Прочтём это операционально. <<Для всякой точности $ε$ >> — какое бы малое расхождение мы ни назвали; <<можно указать $N$ >> — найдётся рубеж; <<любые $m, n \geq N$ >> — начиная с этого рубежа все приближения; << $∣ a_{m} - a_{n} ∣ < ε$ >> — расходятся меньше чем на названную точность. Иными словами: какую угодно тесноту потребуй — процесс рано или поздно в неё войдёт и больше из неё не выйдет. Определение не упоминает предела; оно целиком о внутреннем поведении процесса. Это операциональное, $P 4$ -совместимое условие: оно проверяется по конечным запросам и не нуждается в завершённом объекте.

Число как отобранный процесс

Теперь можно сказать точно, что такое процессное действительное число в первом приближении: это голый процесс, прошедший отбор по свойству Коши. Процесс $0, 1, 0, 1, \dots$ отбор не проходит — для тесноты меньше единицы никакого рубежа $N$ не найти, приближения вечно расходятся на единицу.

Процессы рациональных приближений к $2$ , разобранные в Главе III.4, — ньютонов процесс и процесс подходящих дробей цепной дроби, — служат мотивационными примерами таких кандидатов в числа. Здесь, однако, нужна точность относительно того, что в репозитории об этих процессах доказано. В формализации Главы III.4 для них проверены первые шаги, установлено различие двух процессов и проведено сравнение качества приближения на конкретном шаге. Полное доказательство того, что именно ньютонов или цепно-дробный процесс есть процесс Коши — то есть отдельная теорема вида is_Cauchy с оценкой скорости сходимости, — в проверенном фрагменте не предъявлено и требует самостоятельной формулировки. Глава III.4 поддерживает идею, что к одному числу ведут разные процессы; полная проверка их сходимости в форме Коши — предмет отдельной теоремы. Сказанное здесь о $2$ следует читать в этом точном смысле: $2$ — образцовый кандидат на роль процессного числа, и наглядный, но именно как кандидат.

Здесь, однако, надо быть точным в одном пункте, и это первый случай, где сказывается множественность процессных конструкций в репозитории (о ней § 2.5). Свойство Коши в ToS формализовано двумя предикатами в двух файлах. В CauchyReal.v — предикат is_cauchy, приведённый выше. В ProcessCore.v — предикат is_Cauchy (с заглавной буквой), наложенный на RealProcess. По смыслу это одно и то же условие; формально это два разных предиката в двух разных файлах, и глава не будет делать вид, будто это один. Файл ProcessGeneral.v проводит между ними мост — к нему § 2.5 и вернётся. Пока же запомним содержательное: число есть процесс, прошедший отбор по свойству Коши, — а каким из двух предикатов отбор записан, зависит от того, в какой из процессных линий репозитория мы работаем. В E/R/R-разборе (§ 2.8.2) свойство Коши — это правило отбора, выделяющее из носителей-процессов представителей числа.

Арифметика процессов

Операции поточечны

Над числами нужны арифметические операции. Если процессное действительное число есть процесс, то и операции предстоит вести над процессами — и нужно сказать, что это значит. Rocq-формализация отвечает в файле ProcessArithmetic.v, и ответ прост: операции над процессами поточечны.³ В текущем процессном ядре формализованы аддитивные операции и масштабирование рациональной постоянной: сложение, противоположный процесс, вычитание и умножение на рациональное число. Сложить два процесса значит сложить их приближения на каждом шаге порознь:

Definition process_add (R1 R2 : RealProcess) : RealProcess :=
  fun n => R1 n + R2 n.
 
Definition process_neg (R : RealProcess) : RealProcess :=
  fun n => - (R n).
 
Definition process_sub (R1 R2 : RealProcess) : RealProcess :=
  fun n => R1 n - R2 n.
 
Definition process_scale (c : Q) (R : RealProcess) : RealProcess :=
  fun n => c * R n.

Сумма процессов $R_{1}$ и $R_{2}$ на шаге $n$ есть сумма рациональных чисел $R_{1} (n)$ и $R_{2} (n)$ ; противоположный процесс на каждом шаге меняет знак; вычитание и умножение на рациональную постоянную — так же, поточечно. Определения не выходят за пределы рациональной арифметики: на каждом отдельном шаге складываются и умножаются рациональные числа, конечные записи. Бесконечного в этих определениях нет ничего — есть лишь правило, которое поточечную рациональную операцию применяет на всяком шаге по запросу. Арифметика процессов наследует $P 4$ -устройство процесса: она тоже схема, а не завершённый объект.

Стоит сразу отметить границу этого аппарата. Перечисленные операции — аддитивные (сложение, отрицание, вычитание) и масштабирование рациональной постоянной. Полного умножения двух произвольных процессных чисел — операции $R_{1}, R_{2} \mapsto (n \mapsto R_{1} (n) \cdot R_{2} (n))$ с доказательством, что она сохраняет свойство Коши, — среди операций ProcessArithmetic.v нет, и настоящая глава его не строит и не использует. Само умножение, однако, в репозитории построено — отдельным файлом: process_mul с леммой сохранения Коши mul_preserves_Cauchy (CauchyProcessBridge.v), а на упакованной линии — cauchy_mul с полевыми законами (RealField.v). Оно и вправду сложнее сложения (оценка произведения привлекает ограниченность сомножителей) и относится к построению поля — к нему обращается Глава 4.3 (§ 3.6). Здесь же предмет — тип числа и его аддитивная арифметика; умножение эта глава не использует, но открытым направлением оно уже не является.

Операции сохраняют свойство Коши

Поточечное определение операций само по себе ещё ничего не гарантирует. Возникает законный вопрос: если $R_{1}$ и $R_{2}$ суть числа — то есть прошли отбор § 2.3, удовлетворяют свойству Коши, — то будет ли их сумма снова числом? Иначе говоря: не выводит ли арифметика за пределы отобранного класса? Если бы выводила, действительные числа не были бы замкнуты относительно сложения, и вся конструкция теряла бы смысл.

ProcessArithmetic.v доказывает, что не выводит. В файле — четыре теоремы сохранения:

Theorem add_preserves_Cauchy : forall R1 R2,
  is_Cauchy R1 -> is_Cauchy R2 -> is_Cauchy (process_add R1 R2).
Theorem neg_preserves_Cauchy : forall R,
  is_Cauchy R -> is_Cauchy (process_neg R).
Theorem sub_preserves_Cauchy : forall R1 R2,
  is_Cauchy R1 -> is_Cauchy R2 -> is_Cauchy (process_sub R1 R2).
Theorem scale_preserves_Cauchy : forall c R,
  is_Cauchy R -> is_Cauchy (process_scale c R).

Каждая утверждает одно: операция, применённая к процессам Коши, даёт снова процесс Коши. Доказательства — классические $ε$ -рас-суж-де-ния: чтобы сумма уложилась в точность $ε$ , довольно, чтобы каждое слагаемое уложилось в $ε /2$ , и неравенство треугольника для модуля рациональных довершает дело. Существенно не устройство доказательств, а их итог: отобранный класс замкнут относительно арифметики. Складывая, вычитая, масштабируя действительные числа, мы снова получаем действительные числа — не выпадаем из класса, который отбор § 2.3 выделил.

Связь с $P 4$ {P4} Главы 4.1

Стоит заметить, что эти теоремы сохранения перекликаются с тем, что встречалось в Главе 4.1. Там предикат P4_formalized из ProcessFourPrinciples.v был конъюнкцией трёх утверждений: существует процесс Коши; некоторая операция над процессами Коши сохраняет свойство Коши; сумма процессов Коши есть процесс Коши. Третий конъюнкт P4_formalized — это в точности теорема замкнутости относительно сложения, аналогичная приведённой здесь add_preserves_Cauchy.

Второй конъюнкт требует оговорки, и важной. В P4_formalized он записан через process_product и process_fst: сохранение свойства Коши под первой проекцией продукта процессов. Слово product здесь относится к продукту процессов в структурном, категориальном смысле — к образованию пары процессов и её проекциям, — а не к арифметическому умножению двух действительных чисел $R_{1} (n) \cdot R_{2} (n)$ . Глава не смешивает эти две вещи. Арифметическая замкнутость, которую настоящая глава реально использует и которую даёт ProcessArithmetic.v, — это замкнутость относительно сложения, вычитания, отрицания и рационального масштабирования (§ 2.4.2); арифметического умножения двух процессов среди неё, как отмечено в § 2.4.1, нет.

Связь с Главой 4.1 поэтому содержательная, но не буквальная. Глава 4.1 говорила о P4_formalized как о формальном следе принципа $P 4$ — машинно-проверяемом ядре, фиксирующем, что процессы Коши существуют и замкнуты относительно некоторых операций. Настоящий раздел показывает аддитивную замкнутость вблизи, на уровне отдельных теорем ProcessArithmetic.v. То, что в Главе 4.1 было сжато в один предикат-след, здесь развёрнуто в рабочую аддитивную арифметику. Процессное действительное число не просто существует как тип — над ним считают: определены аддитивные операции, и они не разрушают его числовой природы. В терминах § 2.8.2 это правила-операции (Rules), сохраняющие роль <<число>>: отобранный класс замкнут.

Тип действительного числа

Носитель и свидетель в одном объекте

{ До сих пор действительное число описывалось в два приёма: голый процесс (тип RealProcess, § 2.2) плюс условие отбора (свойство Коши, § 2.3). Число было процессом и доказательством того, что процесс прошёл отбор, — но эти две вещи лежали порознь: процесс в одном месте, его свойство Коши в другом. }

Полноценный тип действительного числа сводит их в один объект. В Rocq это делается записью — структурой с полями. Файл CauchyReal.v вводит тип CauchySeq:⁴

Record CauchySeq := mkCauchy {
  cs_seq :> nat -> Q;
  cs_cauchy : is_cauchy cs_seq
}.

Терм типа CauchySeq — это пара: первое поле, cs_seq, — сам процесс, функция из номеров в рациональные; второе поле, cs_cauchy, — доказательство того, что этот процесс удовлетворяет свойству Коши. Конструктор mkCauchy собирает объект из этих двух составляющих: носитель и свидетель отбора вместе.

Здесь нужно сразу сказать точно, чем CauchySeq является, а чем — нет, потому что соблазн назвать его прямо <<типом действительного числа>> велик, а это было бы неточно. CauchySeq есть тип процессных представителей действительных чисел. Терм типа CauchySeq — это процесс рациональных приближений вместе с доказательством его фундаментальности; это кандидат, прошедший отбор, законный представитель некоторого действительного числа. Но собственно число, строго говоря, CauchySeq ещё не есть. Число возникает следующим шагом — как класс эквивалентности таких представителей по отношению cauchy_equiv (о нём § 2.6); этот шаг, факторизацию, совершит Глава 4.3. Различие существенно, и глава будет его держать: RealProcess (§ 2.2) — голый процесс-кандидат; CauchySeq — процесс-представитель, кандидат, прошедший отбор; собственно число — класс эквивалентных представителей.

{ С этой оговоркой видно, чем CauchySeq отличается от RealProcess. Тип RealProcess был шире: он вмещал и расходящиеся процессы, не задающие никакого числа. Тип CauchySeq расходящийся процесс вместить не может: чтобы построить терм типа CauchySeq с данным носителем, нужно предъявить второе поле — доказательство is_cauchy этого носителя; а для процесса, у которого свойство Коши опровергнуто, такого доказательства предъявить нельзя. Поэтому население типа CauchySeq — ровно процессы Коши, то есть допустимые представители действительных чисел, и ничего сверх. Отбор § 2.3 здесь не отдельный шаг, а часть устройства типа. }

Маленькая, но важная деталь записи — двоеточие со стрелкой в cs_seq :> nat -> Q. Это принуждение (coercion): Rocq разрешает применять терм типа CauchySeq прямо как функцию, автоматически беря его первое поле. Если $a$ есть CauchySeq, то $a (n)$ означает cs_seq $a (n)$ — приближение представителя $a$ на шаге $n$ . Представитель можно запрашивать как процесс, не извлекая носитель вручную. Тип помнит, что процессный представитель числа — это всё ещё процесс, только процесс с гарантией.

Конструктивное пополнение рациональных чисел

Стоит назвать вещь её классическим именем. То, что строит CauchyReal.v, — это пополнение поля рациональных чисел по Коши: стандартная конструкция, которой математика получает действительные числа из рациональных. Рациональные числа неполны — в них есть <<дыры>> вроде $2$ , последовательности приближений, которым некуда сойтись внутри $Q$ . Пополнение затыкает дыры, объявляя действительным числом саму сходящуюся последовательность рациональных приближений.

Особенность ToS — не в самой конструкции, а в её прочтении. Классическое изложение говорит: действительное число есть класс эквивалентности фундаментальных последовательностей — готовый объект фактормножества. ToS читает то же построение процессно: CauchySeq есть не точка готового континуума, а процесс с гарантией сходимости. Заголовок файла называет это <<конструктивным пополнением>>: конструктивным — ибо всякий представитель предъявляется явно, своим процессом и своим доказательством, без обращения к завершённой бесконечности. Та же классическая конструкция, прочитанная в духе $P 4$ .

Нужна, впрочем, точность относительно того, что в файле уже построено. Слова о <<классе эквивалентности фундаментальных последовательностей>> — это пока классическое математическое чтение, а не готовый Rocq-объект. Файл CauchyReal.v строит тип представителей CauchySeq и отношение cauchy_equiv; он не строит фактортип — тип, в котором эквивалентные процессы буквально стали бы одним термом. Действительное число как класс эквивалентности есть, стало быть, задача следующего шага, а не уже реализованная в этом файле конструкция. Глава 4.2 даёт представителей и отношение; превращение представителей в числа — факторизацию — совершит Глава 4.3.

Три линии процесса в репозитории

Теперь глава обязана сказать прямо то, на что несколько раз намекала. <<Процесс как тип>> представлен в Rocq-формализации ToS не одной конструкцией, а тремя родственными, и читатель, открыв репозиторий, встретит все три. Честность требует их назвать и показать, как они соотносятся.

Первая линия — RealProcess := nat -> Q из ProcessCore.v (§ 2.2). Голый процесс: функция без вшитого доказательства. На нём стоит арифметика ProcessArithmetic.v (§ 2.4) и формальный след $P 4$ из ProcessFourPrinciples.v (Глава 4.1). Свойство Коши здесь — отдельный предикат is_Cauchy, накладываемый извне.

Вторая линия — CauchySeq из CauchyReal.v (§ 2.5.1). Процесс с вшитым доказательством Коши; тип процессных представителей действительного числа. Своя арифметика (cauchy_add и прочие, § 2.6), своё отношение эквивалентности, свои алгебраические законы. Эта линия в репозитории выросла самостоятельно: CauchyReal.v даже не подключает ProcessCore.v.

Третья линия — GenProcess A := nat -> A из ProcessGeneral.v (§ 2.2.3). Универсальный процесс над произвольным типом $A$ . Это не конкурент первым двум, а рамка над ними: и RealProcess, и носитель CauchySeq суть частные случаи GenProcess при $A = Q$ . Шапка файла прямо говорит, что GenProcess A — универсальный процессный тип, а конкретные процессы суть его частные случаи.

Три линии удобно свести в таблицу — тем более что предикаты Коши у них носят похожие, легко смешиваемые имена:

Файл	Тип	Предикат Коши	Статус
`Process\-Core.v`	`RealProcess`, т. е. `nat -> Q`	`is_Cauchy`	Голый процесс $+$ внешний отбор
`Cauchy\-Real.v`	`CauchySeq`	`is_cauchy`	Процесс $+$ вшитое доказательство
`Process\-Gene\-ral.v`	`GenProcess A`, т. е. `nat -> A`	`is_cauchy_gen`	Общая метрическая рамка

Заметим и устройство репозитория: CauchyReal.v и ProcessGeneral.v лежат в верхнем каталоге src/, а ProcessCore.v — в src/process/. Это историческое расположение файлов; концептуально все три принадлежат одному процессному слою.

Как три линии соотносятся

Соотношение трёх линий ProcessGeneral.v не оставляет догадкам — оно его частично доказывает. Файл вводит рациональную метрику Qdist $x y := ∣ x - y ∣$ и общее свойство Коши is_cauchy_gen относительно произвольной метрики, после чего доказывает лемму cauchy_Q_equiv:

Lemma cauchy_Q_equiv : forall (a : nat -> Q),
  is_cauchy a <-> is_cauchy_gen Qdist a.

{ Левая часть — предикат is_cauchy из CauchyReal.v; правая — общее свойство Коши при метрике Qdist. Лемма устанавливает их равносильность: свойство Коши второй линии есть частный случай общего свойства Коши третьей. Следующая лемма, cauchy_seq_is_gen_process, довершает: всякий CauchySeq есть GenProcess $Q$ , удовлетворяющий общему свойству Коши. }

{ Стоит проследить связь линий до конца. ProcessGeneral.v связывает вторую и третью линии — предикат is_cauchy с is_cauchy_gen. Первую же со второй связывает теперь отдельный файл CauchyProcessBridge.v: предикаты is_Cauchy (из ProcessCore.v, первая линия) и is_cauchy (из CauchyReal.v, вторая) формализуют одно и то же $ε$ - $N$ -условие и оказались совпадающими буквально, — так что мостовая лемма is_Cauchy_iff_is_cauchy ( $‘ i s_{C} a u c h y ‘ R \leftrightarrow ‘ i s_{c} a u c h y ‘ R$ для всякого $R$ ) доказывается простой развёрткой определений. Лемма process_equiv_iff_cauchy_equiv связывает и отношения эквивалентности двух линий, а функция to_CauchySeq переводит процесс первой линии в представитель второй. }

Это снимает прежнюю оговорку: направление синхронизации, которое глава здесь называла, пройдено. Мостовая лемма <<для всякого $R$ верно is_Cauchy $R$ тогда и только тогда, когда is_cauchy $R$ >> построена (is_Cauchy_iff_is_cauchy), и при полном совпадении определений её доказательство и свелось к развёртке. Операции переносятся по тому же мосту: умножение второй линии cauchy_mul даёт умножение первой process_mul — с сохранением Коши и совместимостью (CauchyProcessBridge.v). Так что первая и вторая линии — не <<родственные, но формально раздельные>>, а машинно связанные: переход между ними теперь есть ссылка на доказанное, а не только содержательный жест. Различие же остаётся онтологическим, а не формальным — это две записи одного $ε$ - $N$ -условия, и мост именно записи и отождествляет.

Какую линию глава берёт за основную

Раз линий три, нужно сказать, на какой из них стоит дальнейшая Часть IV. Глава делает выбор и называет его явно.

Основным типом для построения процессного действительного числа глава берёт CauchySeq — вторую линию. Причина проста: именно CauchySeq есть готовый тип представителей, снабжённый всем нужным аппаратом. В нём доказательство Коши вшито в объект, а не приложено снаружи; его население — ровно процессы Коши, допустимые представители чисел; для него уже доказаны отношение эквивалентности со всеми нужными свойствами и алгебраические законы (§ 2.6). Когда Глава 4.3 будет строить число как класс эквивалентности, а Глава 4.4 — доказывать несчётность, удобнее всего опираться на тип представителей, который уже несёт свою гарантию внутри.

При этом RealProcess не отбрасывается. Он остаётся в изложении как голый процесс — процесс до наложения условия Коши, то самое широкое пространство § 2.2, внутри которого представители выделяются отбором. Различие линий получает теперь ясный смысл, и его стоит назвать в окончательной форме: RealProcess — голый процесс-кандидат; CauchySeq — процесс-представитель, кандидат, прошедший отбор; собственно число — класс эквивалентных представителей, и его строит Глава 4.3. А GenProcess остаётся универсальной рамкой, напоминающей, что и то и другое — частные случаи одной идеи процесса над типом. Глава не сводит три линии в одну искусственно — она расставляет их по ролям: рамка, кандидат, представитель, — а число оставляет следующей главе.

Когда два процесса задают одно число

Разные процессы, одно число

Глава III.4 уже отметила — а Глава 4.1 повторила, — что у одного действительного числа процессов много. К $2$ ведёт не один процесс рациональных приближений, а разные: можно приближать $2$ десятичными дробями, можно — подходящими дробями цепной дроби, можно — ньютоновыми итерациями. Это разные процессы — разные функции из номеров в рациональные, дающие на одних и тех же шагах разные приближения. Но число они задают одно.

Значит, тип CauchySeq различает больше объектов, чем есть действительных чисел: одному числу отвечает целое семейство термов типа CauchySeq. Это и есть та причина, по которой § 2.5 называл CauchySeq типом представителей, а не самих чисел: представителей у одного числа много. Чтобы от представителей перейти к числам, нужно отождествить процессы, задающие одно и то же. Нужно отношение: <<процесс $a$ и процесс $b$ задают одно число>>.

Отношение эквивалентности процессов

Когда два процесса Коши задают одно число? Тогда, когда их приближения со временем сближаются неограниченно — расходятся меньше всякой наперёд заданной точности. Это — то же $ε$ - $N$ -рассуждение, что в свойстве Коши, только теперь применённое к паре процессов. CauchyReal.v вводит его как предикат cauchy_equiv:

Definition cauchy_equiv (a b : CauchySeq) : Prop :=
  forall eps : Q, 0 < eps ->
    exists N : nat, forall n : nat,
      (N <= n)%nat -> Qabs (cs_seq a n - cs_seq b n) < eps.

Процессы $a$ и $b$ эквивалентны, если для всякой точности $ε$ найдётся рубеж $N$ , начиная с которого их приближения расходятся меньше чем на $ε$ . Файл вводит для этого отношения знак — $a \sim \sim b$ (в записи репозитория — a \~{}\~{} b).

{ Чтобы такое отношение годилось для отождествления чисел, оно должно быть отношением эквивалентности — рефлексивным, симметричным, транзитивным. CauchyReal.v это и доказывает, тремя отдельными леммами: cauchy_equiv_refl (всякий процесс эквивалентен себе), cauchy_equiv_sym (если $a$ эквивалентен $b$ , то $b$ — $a$ ), cauchy_equiv_trans (если $a$ эквивалентен $b$ , а $b$ — $c$ , то $a$ — $c$ ). Три свойства доказаны; cauchy_equiv есть полноценное отношение эквивалентности на типе CauchySeq. }

Арифметика уважает эквивалентность

Одного отношения эквивалентности мало — нужно ещё, чтобы оно было согласовано с арифметикой. Если число можно задавать разными процессами, то результат сложения не должен зависеть от того, какие именно процессы-представители мы взяли. Сложив $a$ с $b$ и сложив эквивалентный $a$ процесс $a^{'}$ с эквивалентным $b$ процессом $b^{'}$ , мы обязаны получить эквивалентные результаты — иначе сложение не было бы операцией над числами, а лишь над процессами.

{ CauchyReal.v доказывает и это. Файл определяет арифметику второй линии — cauchy_add, cauchy_neg, cauchy_sub, cauchy_const, — где каждая операция есть mkCauchy: она строит новый CauchySeq, сразу снабжая результат доказательством, что он опять Коши (это та же замкнутость, что в § 2.4, но проведённая внутри второй линии). А затем — ключевые леммы согласования: }

Lemma cauchy_add_compat : forall a a' b b' : CauchySeq,
  a ~~ a' -> b ~~ b' -> cauchy_add a b ~~ cauchy_add a' b'.
Lemma cauchy_neg_compat : forall a a' : CauchySeq,
  a ~~ a' -> cauchy_neg a ~~ cauchy_neg a'.

Лемма cauchy_add_compat говорит: замена слагаемых на эквивалентные даёт эквивалентную сумму; cauchy_neg_compat — то же для смены знака. Арифметика уважает отношение эквивалентности. Это значит, что операции корректно определены не только на процессах, но и на числах — на классах эквивалентных процессов: результат не зависит от выбора представителя.

Что это готовит для Главы 4.3

Сложенное в этом разделе — прямой мост к следующей главе. CauchySeq даёт процессы; cauchy_equiv говорит, какие из них задают одно число; рефлексивность, симметрия, транзитивность делают это отношение настоящей эквивалентностью; леммы согласования обеспечивают, что арифметика переживает переход к классам. Всё готово для шага, который сделает Глава 4.3: объявить действительное число классом эквивалентности процессов, а точку — не исходным объектом, а именно таким классом, режимом рассмотрения, в который оператор переходит, отвлекаясь от различий между процессами с общим пределом. Настоящая глава построила тип и снабдила его отношением; Глава 4.3 совершит факторизацию.

Структурные признаки сходимости

Зачем нужны достаточные условия

Свойство Коши § 2.3 — определение: оно говорит, что значит быть сходящимся процессом. Но проверять его прямо по определению — для всякой точности $ε$ искать рубеж $N$ — не всегда удобно. Часто процесс устроен так, что его сходимость видна из структуры, без перебора $ε$ . Математике поэтому нужны достаточные условия Коши: структурные признаки, из которых свойство Коши следует. Rocq-формализация ToS такие признаки даёт, и настоящий раздел собирает главные.

Монотонность и ограниченность

Первый и важнейший признак — классический. Процесс называется монотонно возрастающим, если каждое следующее приближение не меньше предыдущего, и монотонно убывающим — если не больше. ProcessArithmetic.v вводит оба понятия:

Definition monotone_increasing (R : RealProcess) : Prop :=
  forall n, R n <= R (S n).
Definition monotone_decreasing (R : RealProcess) : Prop :=
  forall n, R (S n) <= R n.

И доказывает признак сходимости — теорему monotone_bounded_Cauchy:

Lemma monotone_bounded_Cauchy : forall R ub,
  monotone_increasing R -> (forall n, R n <= ub) -> is_Cauchy R.

Монотонно возрастающий процесс, ограниченный сверху некоторым рубежом $u b$ , есть процесс Коши. Двойственная теорема, decreasing_bounded_Cauchy, утверждает то же для монотонно убывающего, ограниченного снизу. Содержательно это знакомый принцип: последовательность, которая всё время растёт, но не может перевалить за потолок, обязана сойтись — ей просто некуда деться, кроме как скучиться у некоторого значения. Признак мощный: он сводит проверку сходимости к двум структурным фактам — монотонности и ограниченности, — ни один из которых не требует перебора $ε$ .

Доказательство в файле опирается на архимедовость рациональных чисел — лемму q_archimedean: для любого рубежа $d$ и любой положительной величины $ε$ найдётся натуральное $K$ , для которого $K ε$ превосходит $d$ . Это важная техническая опора: именно архимедовость не даёт монотонному ограниченному процессу <<зависнуть>>, не дойдя до скучивания. ProcessArithmetic.v архимедовость не постулирует, а доказывает — через целочисленное деление.

Здесь нужна оговорка о логическом статусе, и глава её делает. В отличие от базового файла CauchyReal.v, доказательство monotone_bounded_Cauchy в ProcessArithmetic.v использует классическую логику: в коде применяется разбор случаев через classic (файл импортирует Classical). Для ToS это не новая внешняя аксиома — classic есть уже принятый закон $L 3$ (Глава 4.1, § 1.2.4), — но статус этого доказательства следует отличать от полностью конструктивных лемм. CauchyReal.v с его базовой конструкцией CauchySeq, отношением cauchy_equiv и аддитивной арифметикой обходится без classic вовсе; структурный же критерий monotone_bounded_Cauchy опирается на $L 3$ . Глава отмечает это, чтобы не выдать классический критерий за конструктивный в том же смысле, в каком конструктивно базовое построение типа.

Геометрическая скорость: процессный зазор

{ Второй признак — иной природы и связан с скоростью сходимости. Файл ProcessBounds.v вводит структуру, которую можно назвать процессным зазором.⁵ Это запись has_process_mass_gap с тремя условиями: процесс имеет устойчивый положительный нижний рубеж; его приближения сходятся с геометрической скоростью — расхождение убывает как степень некоторого числа меньше единицы; и процесс монотонно убывает. }

Имя mass_gap стоит читать как технический термин процессной формализации — наличие положительного нижнего зазора и геометрической оценки скорости. Это не утверждение о физическом массовом зазоре в смысле квантовой теории поля; оговорка нелишняя, поскольку в репозитории ToS есть и файлы физического содержания, и читатель мог бы связать имена. Здесь mass_gap — чисто структурное понятие сходимости.

Главная теорема файла — pmg_implies_cauchy: процесс с таким зазором есть процесс Коши. Геометрическая скорость — очень сильное структурное условие: если расхождение приближений убывает как $r^{n}$ при $r < 1$ , сходимость не просто гарантирована, она быстра. Но условие это достаточное, а не необходимое: процессный зазор — не критерий сходимости вообще, а лишь один из путей к ней. Существуют процессы Коши, у которых нет ни положительного нижнего рубежа, ни геометрической скорости, — и файл это прямо показывает: теоремы pathological_no_pmg и vanishing_no_pmg устанавливают, что у нулевого процесса и у процесса, убывающего к нулю, такого зазора нет. Условие зазора содержательно: оно выполнено для части сходящихся процессов, не для всех. Глава приводит его как один из структурных признаков Коши — не столь универсальный, как монотонность с ограниченностью, и не как главный.

Полнота: процесс приближается рациональными

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

Здесь нужна точность в том, что именно доказано. Эти две теоремы фиксируют базовую форму полноты конструкции: каждый CauchySeq сам предоставляет рациональные приближения и сходится к себе как процессному объекту. Это ещё не полная метатеорема о метрической полноте — не утверждение <<всякая фундаментальная последовательность процессных действительных чисел имеет пределом процессное действительное число>>. Такая теорема потребовала бы отдельной формулировки: последовательностей действительных чисел, их пределов, и доказательства, что предел снова есть действительное число. cauchy_rational_approx и cauchy_complete_self к ней не равны; полная метрическая полнота пространства классов CauchySeq — отдельная задача, выходящая за пределы Главы 4.2. Содержательно же сказанного довольно для главного: рациональные числа неполны (в них $2$ <<не помещается>>), а процессная конструкция эту неполноту устраняет на базовом уровне — всякий процесс Коши имеет, к чему сходиться, к самому себе. И этот базовый результат доказан без завершённой бесконечности: CauchyReal.v в своей основе несёт ноль аксиом, построение конструктивно над $Q$ .

Тип построен

Что сделано

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

Сперва — голый процесс: тип RealProcess как функция из номеров шагов в рациональные приближения, наблюдаемая по конечным префиксам (§ 2.2). Затем — осознание, что голый процесс слишком широк: тип RealProcess вмещает и расходящиеся процессы, не задающие никакого числа, и потому нужен отбор — свойство Коши, $ε$ - $N$ -условие о внутреннем сближении приближений (§ 2.3). Затем — арифметика: поточечные аддитивные операции и теоремы о том, что отбор они переживают, отобранный класс замкнут относительно сложения, вычитания, масштабирования (§ 2.4). Затем — тип процессных представителей действительного числа CauchySeq: запись, сводящая процесс и доказательство его сходимости в один объект, так что население типа — ровно процессы Коши, допустимые представители чисел (§ 2.5). Затем — отношение эквивалентности, говорящее, когда два процесса задают одно число, с доказанными рефлексивностью, симметрией, транзитивностью и согласованностью с арифметикой (§ 2.6). Наконец — структурные признаки, позволяющие устанавливать сходимость, не перебирая $ε$ (§ 2.7).

Глава честно показала и то, что <<тип процесса>> в репозитории ToS существует в трёх родственных оформлениях — голый RealProcess, снабжённый гарантией CauchySeq, универсальная рамка GenProcess, — и расставила их по ролям: кандидат, представитель, рамка. Основным типом для построения процессного действительного числа во всей дальнейшей Части IV глава приняла CauchySeq — с ясной оговоркой, что собственно число есть класс эквивалентных представителей, и шаг к нему сделает Глава 4.3.

Разбор E/R/R: процессное число как система

Слои, перечисленные только что, складываются в систему — процессное действительное число, — и эта система имеет E/R/R-устройство (Часть I). Соберём его разбор; он лишь называет в терминах E/R/R то, что глава уже построила. Заголовки опорных файлов задают разметку прямо: ProcessCore.v объявляет правило — всякий объект есть конечный процесс на каждой стадии ( $P 4$ ); ProcessArithmetic.v — каждая операция сохраняет свойство Коши.⁶ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: <<система>> — содержательная интерпретация; речь идёт о процессах и представителях над $Q$ , а собственно число как класс ещё не построено — его даёт Глава 4.3.

Rules — правила (закон $L 5$ ). Конституция — принцип $P 4$ : число есть не завершённая точка, а процесс рациональных приближений, конечный на каждой стадии; из неё следует и само устройство носителя — функция nat -> Q (§ 2.2). К конституции примыкает конкретный слой правил: свойство Коши как правило отбора (что годится в число, § 2.3); поточечная арифметика, замкнутая относительно Коши (§ 2.4); отношение эквивалентности с согласованностью с арифметикой — правило <<когда два процесса задают одно число>> (§ 2.6); структурные признаки сходимости (§ 2.7). Честная граница: критерий monotone_bounded_Cauchy опирается на $L 3$ (не на чистую конструкцию). Полного умножения двух процессов среди правил этой главы нет — но в репозитории оно построено (process_mul, cauchy_mul; § 2.4.3 и Глава 4.3).

Roles — значимость позиций (закон $L 4$ ). Здесь — центральное различение всей главы, прочитанное как ролевые статусы. Один и тот же носитель-процесс проходит три роли: голый кандидат (RealProcess — процесс до отбора), представитель, прошедший отбор по Коши (CauchySeq — процесс с вшитой гарантией), и, наконец, число — класс эквивалентных представителей. По $L 4$ каждый статус обоснован своим правилом: отбор Коши делает процесс представителем, эквивалентность собирает представителей в число. Эта прогрессия ролей — кандидат $\to$ представитель $\to$ число — и есть стержень главы.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — рациональные приближения $a (n)$ на каждом шаге; сам носитель есть процесс nat -> Q, простейший — постоянный const_process. По $L 1$ каждое приближение тождественно себе. По $P 4$ носитель конечен на любом уровне: процесс наблюдается префиксами — конечными списками длины $n$ (§ 2.2.3), а не предъявляется весь.

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

Компонент	Что фиксирует	E/R/R
приближения $a (n)$ ; процесс `nat -> Q`	носители (конечны, $P 4$ )	Element
статусы: кандидат $\to$ представитель $\to$ число	ролевые позиции	Role
$P 4$ : объект есть конечный процесс на стадии	конституция	Rule
свойство Коши	правило отбора	Rule (конкр.)
поточечная арифметика (сохраняет Коши)	правила операций	Rule (конкр.)
эквивалентность $+$ согласованность	правило <<то же число>>	Rule (конкр.)
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: приближения и процесс суть элементы, статусы кандидат/представитель/число — роли, $P 4$ с Коши и арифметикой — правила. Самореференции нет. Две честные оговорки. Во-первых, роль <<число>> на уровне этой главы ещё не реализована: построены носитель и представители, а число как класс строит Глава 4.3, — так что система здесь хорошо сформирована на уровне представителей. Во-вторых, <<неизбежность>> типа (§ 2.8.3 ниже) — содержательный тезис, не Rocq-теорема о единственности конструкции.

{ Этот разбор — E/R/R-фундамент всей Части IV. Он показывает, что RealProcess, CauchySeq и число — не три конкурирующих определения, а три ролевых статуса одного носителя, связанных правилом отбора (Коши) и правилом отождествления (эквивалентность); а $P 4$ — конституция, по которой число вообще есть процесс, а не точка. На этом типе встанут и факторизация Главы 4.3 (число как класс), и весь анализ Части V: метрика, непрерывность, производная, интеграл работают над процессными числами, прочитанными именно так.}

Тип не произволен

Стоит в итоге вернуться к тезису § 2.1: тип процессного действительного числа не произволен. Теперь это видно во всей полноте. Каждый его слой вынужден.

Функция из номеров в рациональные — вынуждена: процессу нужно отвечать на запрос <<приближение на шаге $n$ >>, а объект, сопоставляющий номеру приближение, и есть такая функция; ничего нового сверх уже построенных $N$ и $Q$ она не требует. Условие Коши — вынуждено: без отбора тип вмещал бы расходящиеся процессы, не задающие чисел. Сведение носителя и свидетеля в запись CauchySeq — вынуждено: только так население типа совпадает с допустимыми представителями чисел и ни с чем сверх. Отношение эквивалентности — вынуждено: без него одному числу отвечало бы семейство несведённых представителей. Каждый слой — ответ на определённую необходимость, а не свободный выбор конструктора.

Тут, однако, нужна точная оговорка о том, чем эта <<неизбежность>> является и чем — нет. Rocq подтверждает корректность выбранных определений и доказательств: что тип CauchySeq построен без противоречий, что теоремы о нём доказаны. Rocq не доказывает уникальности этой конструкции среди всех возможных формализаций действительного числа. Математике известны и другие пути — сечения Дедекинда, локализованные действительные числа, интервальные представления; ToS выбирает процессный путь по содержательным причинам, изложенным в Главе 4.1 и в § 2.1, а не потому, что прочие пути формально исключены. Поэтому <<тип не произволен>> и <<тип структурно неизбежен>> — это философско-методологический вывод главы: каждый слой CauchySeq вынужден задачей <<построить число как процесс в духе $P 4$ >>. Это не Rocq-теорема и не утверждение о единственности конструкции вообще. Глава высказывает сильный содержательный тезис и тут же очерчивает его границы — ровно как делала Глава 4.1 с формальным следом $P 4$ .

Мост к Главе 4.3

Тип построен — но одно дело сделано не до конца, и Глава 4.2 оставляет его Главе 4.3 намеренно. Тип CauchySeq различает больше объектов, чем есть действительных чисел: одному числу отвечает целый класс эквивалентных процессов (§ 2.6). Отношение, отождествляющее их, построено и снабжено всеми нужными свойствами — но факторизация по нему, переход от процессов к их классам, ещё не совершён.

Этот переход — предмет Главы 4.3. Она объявит действительное число классом эквивалентности процессов и разберёт, что при таком взгляде становится точкой: точка окажется не исходным объектом, а именно классом — режимом рассмотрения, в который оператор переходит, отвлекаясь от различий между процессами с общим пределом. Там же получит разбор и знаменитое равенство нуля целых девяти в периоде единице. В терминах настоящей главы оно предстанет так: процесс десятичных приближений $0, 9; 0, 99; 0, 999; \dots$ и постоянный процесс cauchy_const 1 — два разных представителя, но один класс эквивалентности, а значит — одно число. Точная форма, которую Главе 4.3 предстоит предъявить, — это определение конкретного представителя для $0, 999 \dots$ , постоянного представителя для единицы и доказательство их эквивалентности по cauchy_equiv: схематически

Definition nine_process : CauchySeq := (* 0.9, 0.99, 0.999, ... *)
Definition one_process  : CauchySeq := cauchy_const 1.
Theorem nine_equiv_one : nine_process ~~ one_process.

Равенство $0, 999 \dots = 1$ окажется, стало быть, не парадоксом, а простым следствием того, что два представителя попали в один класс. Настоящая глава построила тип представителей и отношение cauchy_equiv; Глава 4.3 совершит факторизацию и на ней разберёт этот пример. Глава 4.4 затем докажет несчётность процессов, Глава 4.5 переформулирует вопрос о континууме, Глава 4.6 замкнёт часть.

Настоящая глава дала Части IV её основной строительный материал — тип процессных представителей действительного числа. Всё дальнейшее работает с этим типом.

{Процессный представитель действительного числа есть процесс рациональных приближений, прошедший отбор по свойству Коши, взятый как объект единого типа. Rocq-формализация ToS даёт этот тип в трёх родственных оформлениях: голый процесс RealProcess $=$ nat -> Q с внешним предикатом is_Cauchy; снабжённый вшитым доказательством сходимости тип CauchySeq $=$ mkCauchy { cs_seq; cs_cauchy }; универсальная рамка GenProcess A $=$ nat -> A. Эти оформления связаны (лемма cauchy_Q_equiv сводит свойство Коши второй линии к общему случаю третьей), но первая и вторая линии не отождествлены машинно как единый терм; глава расставляет три линии по ролям — кандидат, представитель, рамка — и основным типом для построения числа в Части IV принимает CauchySeq. Существенно: CauchySeq есть тип представителей, а собственно число есть класс эквивалентных представителей; факторизацию совершит Глава 4.3. Над типом определена поточечная аддитивная арифметика — сложение, вычитание, отрицание, рациональное масштабирование, — и доказано, что она сохраняет свойство Коши; полного умножения двух процессов эта глава не строит (оно построено отдельно: process_mul, cauchy_mul). Введено отношение эквивалентности cauchy_equiv с доказанными рефлексивностью, симметрией, транзитивностью и согласованностью с арифметикой — разные процессы могут быть представителями одного числа. Сходимость устанавливается не только по определению, но и структурными признаками — монотонностью с ограниченностью, геометрической скоростью. Базовое построение CauchySeq, отношение cauchy_equiv и аддитивная арифметика в CauchyReal.v несут ноль аксиом и ноль незавершённых доказательств; отдельные структурные критерии — например монотонность с ограниченностью — используют классическую логику $L 3$ , что отмечено особо. Тип не произволен: каждый его слой вынужден задачей построить число как процесс в духе $P 4$ , — это содержательный тезис главы, не Rocq-теорема и не утверждение о единственности конструкции среди всех формализаций действительного числа. Действительное число как класс эквивалентности представителей, и точка как такой класс, строит Глава 4.3.}

Часть: Часть IV. Процессные действительные числа · Том: «Математика»

Понятия: Формализация

Навигация: ← Глава 1. P4: бесконечность как процесс · Глава 3. Точка как класс эквивалентности процессов →

ProcessCore.v Rocq-репозитория ToS (каталог src/process/). Файл объявлен в репозитории как единый источник базовых процессных определений. Имена RealProcess, is_Cauchy, const_process, process_equiv, используемые ниже, — из него. ↩
ProcessGeneral.v Rocq-репозитория ToS (каталог src/), 16 доказанных утверждений, 0 Admitted, 0 аксиом. Файл строит общую теорию процесса над произвольным типом; подробнее о нём § 2.5. ↩
ProcessArithmetic.v Rocq-репозитория ToS (каталог src/process/), 13 доказанных утверждений, 0 Admitted. Файл работает с типом RealProcess из ProcessCore.v. О статусе аксиом — оговорка в § 2.7.2. ↩
CauchyReal.v Rocq-репозитория ToS (каталог src/), 18 доказанных утверждений, 0 Admitted, 0 аксиом. Заголовок файла: <<Cauchy reals: constructive completion of $Q$ >> — конструктивное пополнение рациональных чисел. ↩
ProcessBounds.v Rocq-репозитория ToS (каталог src/process/), 11 доказанных утверждений, 0 Admitted, 0 аксиом. В оригинале структура называется has_process_mass_gap; русское <<процессный зазор>> передаёт смысл — наличие устойчивого положительного нижнего рубежа. ↩
E/R/R-разметка в шапках ProcessCore.v и ProcessArithmetic.v; здесь разворачивается по образцу Части I. ↩

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

Проводник