Глава 3. Точка как класс эквивалентности процессов

От представителей к числу

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

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

И на последнем шаге Глава 4.2 сделала важную оговорку, ради которой и писалась настоящая глава. Тип CauchySeq — это тип представителей действительного числа, а не самих чисел. Представителей у одного числа много: к $2$ ведут и десятичные приближения, и подходящие дроби цепной дроби, и ньютоновы итерации — разные процессы, разные термы типа CauchySeq, — а число они задают одно. Глава 4.2 построила представителей и снабдила их отношением <<задавать одно число>>; но собственно число — то, что получается, когда мы перестаём различать эквивалентных представителей, — она намеренно оставила следующей главе.

Незавершённый шаг: факторизация

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

Глава 4.2 подготовила для этого шага всё необходимое. Отношение cauchy_equiv доказано рефлексивным, симметричным и транзитивным — то есть оно есть полноценное отношение эквивалентности, по которому факторизация корректна. Аддитивная арифметика доказана согласованной с этим отношением — значит, операции переживут переход к классам. Не хватает только самого перехода: объявления, что действительное число есть класс эквивалентности, и разбора того, что при таком объявлении происходит с понятием точки.

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

Настоящая глава этот шаг делает — и делает его не как чисто техническую операцию, а как онтологический поворот. Если число есть класс процессов, то точка — точка действительной прямой, привычный атом непрерывной величины — перестаёт быть исходным объектом. Она оказывается производной: классом эквивалентных процессов, режимом рассмотрения, в который оператор переходит, отвлекаясь от различий между процессами с общим пределом.

Дальнейшее идёт так. Сначала — почему точка вообще не может быть первичной в $P 4$ -онтологии (§ 3.2). Затем — отношение <<задавать одно число>> и его доказанные свойства (§ 3.3), и сразу за ним — то, что Глава 4.2 наметила, а здесь нужно развернуть: две репрезентации процесса, CauchySeq и RealProcess, формально связаны мостом (§ 3.3.1). Затем — класс эквивалентности как точка (§ 3.4) и точка как режим, а не объект (§ 3.5). Затем — что происходит с арифметикой и порядком при переходе к классам (§ 3.6). Затем кульминация — разбор равенства нуля целых девяти в периоде единице (§ 3.7). Наконец — итог и мост к Главе 4.4 (§ 3.8).

Глава, как и предыдущие, сверяется с Rocq-формализацией построчно, и здесь придётся быть особенно точным в одном пункте — различении сетоида и фактортипа. Сетоид — тип представителей вместе с отношением эквивалентности на нём — в репозитории ToS теперь формализован: файл RealPointSetoid.v регистрирует cauchy_equiv как Equivalence, именует носитель RealPoint := CauchySeq и доказывает, что операции суть морфизмы (Proper), уважающие эквивалентность. Сам же фактортип — новый тип, в котором эквивалентные процессы стали бы буквально одним термом, — отдельным объектом не построен, и сознательно: он реифицировал бы режим в вещь и потребовал бы аксиом (§ 3.4.3). Глава не выдаёт одно за другое: <<точку как класс>> она ведёт на формализованном сетоиде, а реификацию в фактортип честно оставляет в стороне как путь, от которого ToS отказывается по $P 4$ . Это — продолжение той же линии точности, которую вели Главы 4.1 и 4.2.

Почему точка не может быть первична

Привычная картина: точка как атом прямой

В привычной математической картине точка первична. Действительная прямая мыслится как совокупность точек, уже собранных воедино; точка — её неделимый атом, готовый объект, который просто есть. Число $2$ при таком взгляде — это определённая точка, занимающая своё место на прямой между $1, 41$ и $1, 42$ ; процессы рациональных приближений лишь указывают на неё, подбираются к готовому месту, которое существовало до всякого приближения.

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

Чего нет и что есть

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

Это, однако, не значит, что в метаязыке нельзя ввести символ или тип, называемый $R$ . Ввести его можно — математика это и делает. Запрет $P 4$ направлен не против символа, а против определённого его чтения: $R$ не должен читаться как первичная завершённая совокупность точек, существующая сама по себе. В ToS такой символ должен быть восстановлен — получить смысл как режим работы с процессами, а не как готовая данность. Различие то же, что Глава 4.1 проводила для типа nat и Глава 4.2 — для RealProcess: формальный объект языка существует, но читается операционально, а не как завершённая актуальная бесконечность.

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

Значит, порядок построения обратный привычному. Не <<есть прямая из точек, процессы к точкам сходятся>>, а <<есть процессы, и точка должна быть из них построена>>. Точка не первее процесса; точка — позднее процесса, она результат некоторой операции над процессами. Какой именно операции — покажут следующие разделы; но уже сейчас ясно, что точка не может быть положена до процессов, она может быть только получена из них.

Точка как восстановимый режим

Здесь важно не впасть в обратную крайность. Сказать <<готовых точек нет>> не значит сказать, что понятие точки бессмысленно или что от него надо отказаться. Глава 4.1 в § 1.8 уже наметила правильную формулировку: точка не отменяется — она восстанавливается позднее, как производный режим. Глава 4.2 в § 2.8 повторила это, указав на факторизацию как на механизм восстановления.

Точка, стало быть, — законное понятие, но не на том месте, на котором её привыкли видеть. Она не фундамент, а надстройка; не вход в конструкцию, а её результат. $P 4$ -онтология не вычёркивает точку, а переставляет её: из первичных объектов — в производные. Настоящая глава эту перестановку и проводит: показывает, какой именно операцией над процессами точка восстанавливается и чем она при таком восстановлении оказывается. Операция эта — факторизация по отношению эквивалентности, и к самому отношению мы теперь и переходим.

Отношение <<задавать одно число>>

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

Чтобы построить точку из процессов, нужно знать, какие процессы отождествлять. Два процесса задают одно число, когда их приближения со временем сближаются неограниченно — расходятся меньше всякой наперёд заданной точности. Глава 4.2 уже ввела это отношение; здесь оно становится рабочим инструментом, и стоит привести его точно. В файле 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.

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

Не поточечное равенство

Здесь нужно сразу предупредить смешение, которое легко совершить. cauchy_equiv не требует, чтобы процессы совпадали на каждом шаге. Оно говорит лишь о пределе расхождения: разность $∣ a_{n} - b_{n} ∣$ должна со временем уйти ниже всякого $ε$ , но на любом конкретном шаге она может быть отлична от нуля.

Различие принципиальное. Поточечное равенство процессов — << $a_{n} = b_{n}$ для всякого $n$ >> — это совсем другое, гораздо более строгое отношение. Два процесса могут задавать одну точку, не совпадая ни на одном конечном шаге: достаточно, чтобы их расхождение убывало к нулю. Именно это и сделает возможным разбор равенства $0, 999 \dots = 1$ в § 3.7 — там два процесса не совпадут нигде, а число зададут одно. Отношение <<задавать одно число>> — это cauchy_equiv, отношение об общем пределе, а не о поточечном тождестве.

Три свойства, делающие отношение пригодным

Чтобы отношение годилось для факторизации — для построения точки как класса, — оно должно быть отношением эквивалентности: рефлексивным, симметричным, транзитивным. Это не формальная придирка, а содержательное требование. Рефлексивность: всякий процесс задаёт то же число, что он сам, — иначе процесс не принадлежал бы своему собственному классу. Симметричность: если $a$ задаёт то же число, что $b$ , то и $b$ — то же, что $a$ , — иначе <<быть одной точкой>> не было бы взаимным. Транзитивность: если $a$ и $b$ задают одно, и $b$ и $c$ задают одно, то $a$ и $c$ задают одно, — иначе классы не были бы устойчивы, представители <<перетекали>> бы между ними.

CauchyReal.v доказывает все три. Это леммы cauchy_equiv_refl, cauchy_equiv_sym и cauchy_equiv_trans. Доказательства — стандартные $ε$ -рассуждения: рефлексивность тривиальна (разность нулевая), симметричность опирается на $∣ - x ∣ = ∣ x ∣$ , транзитивность — на неравенство треугольника с делением $ε$ пополам. Существенно не устройство доказательств, а их итог: cauchy_equiv есть полноценное, машинно-проверенное отношение эквивалентности на типе представителей CauchySeq. Это формальная опора всего дальнейшего: именно потому, что три свойства доказаны, факторизация по cauchy_equiv будет корректной операцией, а не произвольным объединением процессов в группы.

Две репрезентации одного процесса: `CauchySeq`{CauchySeq} и `RealProcess`{RealProcess}

{ Прежде чем строить из этого отношения точку, нужно разобрать одно обстоятельство, которое Глава 4.2 наметила, а здесь оно становится существенным. Глава 4.2 показала, что процесс в репозитории ToS представлен не одной конструкцией: есть голый RealProcess $=$ nat -> Q из ProcessCore.v и есть снабжённый доказательством CauchySeq из CauchyReal.v. И на каждой из двух линий есть своё отношение <<задавать одно число>>: на CauchySeq — разобранное выше cauchy_equiv; на голом RealProcess — предикат process_equiv из ProcessCore.v. }

Важно понять, что process_equiv — это то же самое отношение по смыслу. Его определение в ProcessCore.v:

Definition process_equiv (R1 R2 : RealProcess) : Prop :=
  forall eps : Q, 0 < eps ->
    exists N : nat, forall n : nat,
      (N <= n)%nat -> Qabs (R1 n - R2 n) < eps.

Это тот же критерий общего предела — разность приближений уходит ниже всякого $ε$ , — только записанный для голых процессов. Не нужно путать его с поточечным равенством: как и cauchy_equiv, process_equiv ничего не говорит о совпадении на отдельных шагах. (Поточечное отношение в репозитории тоже есть — например, общий process_equiv с параметром в файле ProcessGeneral.v, требующий согласия на каждом шаге, — но это другая, более строгая линия, и точка строится не по ней.)

{ Раз отношение <<задавать одно число>> есть на обеих линиях, возникает вопрос: согласованы ли они? Если перевести представитель CauchySeq в голый процесс RealProcess, сохранится ли отношение? Ответ Rocq-формализация даёт явно — в файле ProcessBridge.v, чья шапка прямо говорит, что CauchySeq и RealProcess суть один и тот же математический объект.¹ Файл строит два перевода: }

Definition cauchyseq_to_process (cs : CauchySeq) : RealProcess :=
  fun n => cs_seq cs n.
Definition process_to_cauchyseq (R : RealProcess) (H : is_Cauchy R)
  : CauchySeq := mkCauchy R H.

Первый забывает доказательство и оставляет голый процесс; второй, получив процесс вместе с доказательством его фундаментальности, упаковывает их в CauchySeq. И файл доказывает, что эти переводы сохраняют отношение эквивалентности — причём в обе стороны:

Lemma cauchy_equiv_to_process_equiv : forall cs1 cs2 : CauchySeq,
  cauchy_equiv cs1 cs2 ->
  process_equiv (cauchyseq_to_process cs1) (cauchyseq_to_process cs2).
Lemma process_equiv_to_cauchy_equiv : forall cs1 cs2 : CauchySeq,
  process_equiv (cauchyseq_to_process cs1) (cauchyseq_to_process cs2) ->
  cauchy_equiv cs1 cs2.

{

Первая лемма: эквивалентность на CauchySeq влечёт эквивалентность переведённых голых процессов. Вторая — обратное. Вместе они означают, что cauchy_equiv и process_equiv — это одно отношение, увиденное на двух репрезентациях. Файл доказывает и то, что переводы взаимно-обратны: леммы roundtrip_process_equiv и roundtrip_cauchyseq_equiv устанавливают, что перевод туда-обратно возвращает эквивалентный исходному объект. }

{ Для настоящей главы это важно вот чем. Когда дальше глава говорит <<точка есть класс эквивалентности процессов>>, не возникает двусмысленности, каких процессов и по какому отношению. Линия CauchySeq с cauchy_equiv и линия RealProcess с process_equiv не просто похожи — они формально связаны мостом, доказанным в ProcessBridge.v. Точка как класс есть один и тот же объект, на какой бы из двух репрезентаций его ни строить. Глава, как и условлено, ведёт основную линию по CauchySeq; но теперь это выбор репрезентации, а не выбор между разными объектами. }

Класс эквивалентности как точка

Класс процесса

Теперь можно сделать шаг, к которому всё подводилось. Дан процесс — представитель CauchySeq. Рассмотрим все процессы, эквивалентные ему по cauchy_equiv: все, что задают то же число. Эту совокупность назовём классом данного процесса.

Три доказанных свойства отношения (§ 3.3.3) гарантируют, что классы устроены правильно. Рефлексивность: всякий процесс лежит в своём классе. Из симметричности и транзитивности математически следует стандартный факт: два класса либо совпадают целиком, либо не пересекаются вовсе — промежуточного не дано. В файле CauchyReal.v это следствие не выделено отдельной леммой — там доказаны именно cauchy_equiv_refl, cauchy_equiv_sym, cauchy_equiv_trans, — но оно непосредственно вытекает из этих трёх как общее свойство всякого отношения эквивалентности: такое отношение разбивает тип представителей на непересекающиеся классы, и всякий представитель попадает ровно в один. Класс — это <<пучок>> всех процессов с общим пределом, взятый как целое.

И вот определение, ради которого писалась глава: действительное число есть класс эквивалентности процессов; точка — это такой класс. Быть одной точкой значит лежать в одном классе; лежать в одном классе значит задавать один предел. Число $2$ — не атом готовой прямой, а класс: пучок всех процессов рациональных приближений, сходящихся к $2$ , — десятичных, цепно-дробных, ньютоновых, — взятых вместе как один объект.

Что значит <<класс>>: setoid, а не завершённая совокупность

Здесь требуется осторожность, и она прямо вытекает из $P 4$ . Слова <<класс всех процессов, эквивалентных данному>> могут прозвучать так, будто мы образовали новую завершённую совокупность — собрали воедино все эквивалентные процессы как готовый бесконечный объект. Но это вернуло бы завершённую бесконечность, которую вся конструкция как раз обходит. Если бы точка была завершённым множеством процессов, мы не построили бы число без завершённой бесконечности — мы лишь перенесли бы её с прямой на класс.

Поэтому <<класс>> здесь надо понимать иначе — как setoid-класс, а не как completed-совокупность. Сказать <<процесс $a$ принадлежит классу процесса $b$ >> значит ровно одно: $a$ эквивалентен $b$ по cauchy_equiv. Класс — не новый объект, собранный из процессов и положенный поверх них; класс — это режим отождествления: способ смотреть на процессы, при котором эквивалентные не различаются. Точка есть не завершённая совокупность представителей, а тип представителей, взятый вместе с отношением, по которому одни из них считаются за одно. В теории типов такая пара — тип плюс отношение эквивалентности на нём — называется сетоидом (setoid); и <<класс>> в настоящей главе — всегда setoid-класс, режим, а не предмет.

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

Чего глава не утверждает: фактортип не построен

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

В репозитории ToS такого фактортипа нет. Файл CauchyReal.v строит тип представителей CauchySeq и отношение cauchy_equiv; он доказывает рефлексивность, симметричность, транзитивность этого отношения — но не образует тип, термами которого были бы классы. Глава это констатирует прямо и не выдаёт желаемого за сделанное.

{ Существенно, однако, что для содержания настоящей главы фактортип как отдельный Rocq-объект и не требуется — довольно сетоида, и сетоид этот формализован. Файл RealPointSetoid.v регистрирует cauchy_equiv как Equivalence (собирая cauchy_equiv_refl, _sym, _trans в один носитель setoid-структуры), именует точку-носитель RealPoint := CauchySeq и доказывает, что операции суть морфизмы: cauchy_add_Proper и cauchy_mul_Proper уважают эквивалентность. Этого достаточно, чтобы говорить о классах корректно: разбиение на классы есть прямое следствие свойств эквивалентности, а Proper-морфизмы спускают на классы арифметику. <<Точка как класс>> в этой главе — работа с этим формализованным сетоидом, и она вся опирается на доказанное. Построение же фактортипа отдельным типом — не недостающее звено, а путь, от которого ToS осознанно отказывается: реифицированный фактор превратил бы режим отождествления в самостоятельный объект (та самая $P 4$ -ошибка, что и завершённая совокупность, § 3.4.2) и потребовал бы аксиом (у вещественных в Rocq нет канонической формы, равенство неразрешимо). Сетоид — не временная замена фактортипа, а аксиомо-свободная конструкция, которая точке и нужна. }

Точка как режим, а не объект

Сквозной мотив тома

То, что произошло с точкой, не ново для этого тома — это уже случавшийся ход, применённый к новому предмету. Часть I и Часть II проделали то же с множеством: множество в ToS не первичный объект-вместилище, а режим рассмотрения — способ взять различённые элементы под определённым углом, как собранные воедино. Множество не вещь, а взгляд на вещи. В терминах E/R/R (разбор § 3.8.2) и множество, и точка — это роли-режимы, а не элементы.

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

Что теряется и что сохраняется при переходе к классу

Переход от процесса к его классу — это, говоря содержательно, акт отвлечения. Оператор перестаёт обращать внимание на одни черты процесса и оставляет в поле зрения другие. Стоит сказать точно, какие именно.

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

Сохраняется — эквивалентностный инвариант: то, что у всех представителей класса одно и то же в отношении cauchy_equiv. Не конкретный способ движения, а то, что эти движения связаны эквивалентностью — задают, в обычном языке, один и тот же предел, то есть один и тот же класс. Класс есть то в процессе, что не зависит от выбора процесса среди эквивалентных. Точка — это инвариант пучка процессов: то, что у них одно на всех. (Слово <<предел>> здесь — лишь привычное имя этого инварианта; первичен он не как готовая точка, а именно как то общее, что фиксирует отношение cauchy_equiv.)

Точка не беднее процесса

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

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

Арифметика и порядок на классах

Почему нужна согласованность

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

Требование точное: если заменить представители на эквивалентные, сумма обязана остаться в том же классе. На языке § 3.3 это значит, что операции должны уважать отношение cauchy_equiv. Только операции с этим свойством спускаются с представителей на классы — то есть корректно определены на точках.

Сложение и отрицание: совместимость доказана

Для аддитивных операций Rocq-формализация это свойство доказывает прямо. Глава 4.2 уже приводила соответствующие леммы из CauchyReal.v; здесь они получают своё настоящее назначение — обоснование арифметики на классах:

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: то же для смены знака. Значит, сложение и отрицание спускаются на классы: сумма двух точек и точка, противоположная данной, корректно определены, результат не зависит от выбора представителей. Вычитание получается отсюда же — как сложение с противоположным. На классах, стало быть, есть аддитивная арифметика: точки можно складывать, вычитать, брать противоположные, и это операции над числами, а не над случайно выбранными процессами.

Порядок: более слабый, но важный факт

С порядком положение тоньше, и здесь глава скажет ровно то, что доказано, не более. В CauchyReal.v есть отношение cauchy_le — процессное <<меньше либо равно>> — и про него доказана лемма cauchy_le_of_equiv:

Lemma cauchy_le_of_equiv : forall a b : CauchySeq,
  a ~~ b -> cauchy_le a b.

Она говорит: эквивалентные представители связаны отношением cauchy_le (а по симметрии — и в обратную сторону), то есть взаимно неразличимы по этому порядку. Это содержательный и нужный факт: он означает, что эквивалентные процессы не упорядочены строго друг относительно друга — что согласуется с тем, что они задают одно число.

Это — базовое направление: взаимная неразличимость эквивалентных представителей. Полная же совместимость порядка с заменой представителя — утверждение вида: если $a \sim \sim a^{'}$ и $b \sim \sim b^{'}$ , то из cauchy_le $ab$ следует cauchy_le $a^{'} b^{'}$ ; именно она переносит отношение порядка с представителей на классы в полном объёме. Эта лемма — под именем cauchy_le_compat — теперь доказана, в файле RealPointTopology.v, а с нею и cauchy_le_Proper (отношение cauchy_le согласовано с cauchy_equiv в обе стороны). Поэтому итог сильнее, чем глава осторожно намечала: на классы спускается и аддитивная структура (через cauchy_add_compat / cauchy_neg_compat), и отношение порядка (через cauchy_le_compat) — и то, и другое корректно определено на точках, а не только на процессах.

Что это даёт

{ Итог раздела теперь полнее, чем был. Класс эквивалентности — не просто <<пучок процессов>>: на классах есть доказанно корректная кольцевая числовая структура и согласованный порядок. Сложение, вычитание и отрицание спускаются на классы (§ 3.6.2); порядок спускается полностью (cauchy_le_compat, § 3.6.3). Умножение тоже построено: cauchy_mul (файл RealField.v) с доказанными коммутативностью, ассоциативностью, единицей и дистрибутивностью, совместимостью с эквивалентностью (cauchy_mul_compat) и морфизмом cauchy_mul_Proper (RealPointSetoid.v), спускающим его на классы; на голой линии процессов ему отвечает process_mul (CauchyProcessBridge.v). Так что классы можно складывать, вычитать, умножать и сравнивать — и это операции над числами, корректные на точках. Остаётся честная мера: обратный по умножению (cauchy_inv_is_cauchy) определён лишь для отделённых от нуля представителей — деление частично, как и положено конструктивному полю (обратить процесс, лишь эквивалентный нулю, нельзя). Полная полевая структура с тотальным делением — не пробел, который надо закрыть, а граница самого конструктивного понятия числа.² }

Разбор $0, 999 \dots = 1$ {Разбор 0,999… = 1}

Знаменитый <<парадокс>>

Равенство $0, 999 \dots = 1$ — один из самых известных школьных камней преткновения. Интуиция сопротивляется: $0, 999 \dots$ <<выглядит меньше>> единицы, <<не дотягивает>> до неё, между ними будто остаётся бесконечно малый зазор. И всё же математика настаивает, что это одно и то же число.

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

Два процесса

В процессной картине $0, 999 \dots$ — не <<число с бесконечным хвостом девяток>>, а процесс: разворачивающаяся по правилу последовательность рациональных приближений

0, 9; 0, 99; 0, 999; 0, 9999; \dots

На шаге $n$ этот процесс выдаёт рациональное число с $n + 1$ девяткой после запятой. Назовём его десятичным процессом.

Единица — тоже процесс, простейший: постоянный процесс, на каждом шаге выдающий $1$ . В терминах Главы 4.2 это cauchy_const 1.

Это два разных процесса. И разные они не слегка: они различаются на каждом шаге — значение десятичного процесса (nine_raw) на шаге $n$ равно $1 - 1 0^{- (n + 1)}$ , значение постоянного процесса равно $1$ , и эти рациональные числа не совпадают ни при каком $n$ . Это и доказано формально — теорема nine_raw_lt_one: всякая усечёнка строго меньше единицы (§ 3.7.5). И тем не менее два процесса, не совпадающие нигде, задают одно число, лежат в одном классе.

Почему они в одном классе

Они в одном классе потому, что их расхождение уходит к нулю. На шаге $n$ разность между единицей и десятичным процессом есть ровно $1/1 0^{n + 1}$ : единица минус число с $n + 1$ девяткой. А $1/1 0^{n + 1}$ убывает неограниченно: какую угодно тесноту $ε$ ни назови, начиная с некоторого шага расхождение станет меньше $ε$ и дальше уже не выйдет за неё. Это в точности определение cauchy_equiv из § 3.3: десятичный процесс и постоянный процесс эквивалентны.

А раз эквивалентны — они в одном классе. И значит, по определению § 3.4, задают одно число. Равенство $0, 999 \dots = 1$ — это не загадочное совпадение двух разных чисел и не <<соглашение>>; это простая констатация: два разных представителя одного класса. $0, 999 \dots$ и $1$ — два процесса, один пучок, одна точка.

Где был <<парадокс>>

Теперь видно, откуда бралось ощущение парадокса. Оно — порождение точечной картины. Если точка первична, если $0, 999 \dots$ и $1$ суть готовые точки на готовой прямой, то возникает законный вопрос: одна это точка или две? И если две — где между ними зазор; а если одна — почему у неё две разные <<записи>>? Точечная картина ставит вопрос, на который не может внятно ответить, и оттого вопрос ощущается парадоксом.

Процессная картина этого вопроса просто не порождает. В ней $0, 999 \dots$ и $1$ с самого начала суть процессы, и процессы разные — никто и не утверждал, что они один объект на уровне представителей. Вопрос <<одно число или два?>> получает точный смысл: лежат ли два процесса в одном классе эквивалентности? — и точный ответ: да, лежат, ибо их расхождение убывает к нулю. <<Бесконечно малый зазор>>, который интуиция искала между $0, 999 \dots$ и $1$ , — это и есть расхождение $1/1 0^{n + 1}$ ; оно не <<бесконечно малая величина>>, застывшая где-то на прямой, а член процесса, убывающий с шагом. На каждом шаге зазор есть и он положителен; в пределе процесс расхождения уходит ниже всякого $ε$ . Парадокс был артефактом картины, в которой бесконечный процесс приближения подменялся готовой точкой. Убрали подмену — исчез и парадокс. В терминах E/R/R (§ 3.8.2) это было смешением категорий: точку-роль (класс) принимали за элемент-объект.

Формальное доказательство: файл `ProcessNinePoint.v`

Сказанное до сих пор — содержательный разбор. Укажем и формальный статус этого равенства, и здесь глава может быть точной: в репозитории ToS равенство $0, 999 \dots = 1$ доказано как теорема — файл process/ProcessNinePoint.v, теорема nine_equiv_one, без единой аксиомы. Доказательство идёт ровно теми четырьмя шагами, которые набросал содержательный разбор; пройдём их по порядку.

Шаг первый — десятичный процесс как функция из номеров в рациональные:

Definition nine_raw : RealProcess := fun n => 1 - 1 / ten_pow (S n).

Здесь S n — следующее за $n$ число, чтобы нумерация шла с первой девятки: на шаге $n = 0$ процесс даёт $1 - 1/10 = 0, 9$ (машинная проверка nine_raw_0), на шаге $n = 1$ — $1 - 1/100 = 0, 99$ , и так далее. Степень десятки берётся отдельной функцией ten_pow (через pow10 над positive): обычная запись 10 \^{} (S n) над $Q$ в Rocq не сработала бы. Здесь же — машинно проверенное растворение <<парадокса>>: на уровне элементов всякая усечёнка строго меньше единицы (теорема nine_raw_lt_one: forall n, nine_raw n < 1), а на уровне точки процесс совпадает с единицей (шаг четвёртый); <<парадокс>> $0, 999 \dots < 1$ есть смешение этих двух уровней.

{ Шаг второй — доказать, что nine_raw есть процесс Коши. Путь опосредованный, через две репрезентации, и он проведён именно так. Сперва nine_raw берётся как голый RealProcess и доказывается его process_equiv с const_process 1 (шаг четвёртый). Затем из Коши-свойства постоянного процесса (const_is_Cauchy из ProcessCore.v) и леммы equiv_cauchy_l того же файла (эквивалентный процессу Коши процесс сам есть процесс Коши) выводится is_Cauchy nine_raw — теорема nine_raw_is_Cauchy. Тем самым nine_raw при надобности упаковывается в CauchySeq. }

Шаг третий — оценка хвоста: для всякой точности $ε$ найдётся рубеж $N$ , за которым $1/1 0^{n + 1} < ε$ . Содержательно это утверждение о неограниченном росте степеней десятки; технически оно получено из архимедовой леммы q_archimedean (из ProcessArithmetic.v) и оценки роста pow10_ge.

Шаг четвёртый — собрать воедино и доказать целевую теорему:

Theorem nine_equiv_one : nine_raw ~~ const_process 1.

Доказательство есть прямое применение оценки хвоста из шага третьего: расхождение процессов на шаге $n$ равно $1/1 0^{n + 1}$ и уходит ниже всякого $ε$ — значит, по определению process_equiv ( $\sim \sim$ ), процессы именуют одну точку.

Так что писать можно с полным формальным правом: $0, 999 \dots$ и $1$ — разные процессы (разные носители: $‘ nin e_{r} a w ‘0 = 0, 9 \neq = 1$ ), но один класс, одна точка. Теорема доказана на уровне голых процессов ( $‘ nin e_{r} a w ‘ \sim \sim ‘ co n s t_{p} r ocess ‘ 1$ ); перенос на упакованную линию CauchySeq доступен через nine_raw_is_Cauchy и мост, но самим утверждением служит равенство-как-точек на процессах. Формализация не меняет смысла содержательного разбора § 3.7.1–3.7.4, а превращает его в машинно-проверенную теорему: $0, 999 \dots = 1$ есть равенство точек ( $\sim \sim$ ), не тождество объектов ( $=$ ) — процессы различны, точка одна.

Точка построена

Что сделано

Глава начала с шага, который Глава 4.2 оставила незавершённым: факторизации. Тип представителей CauchySeq и отношение cauchy_equiv были построены раньше; настоящая глава выполнила этот переход на setoid-уровне, и сетоид этот теперь формализован (RealPointSetoid.v: Equivalence + Proper-морфизмы): действительное число прочитано как setoid-класс представителей по отношению cauchy_equiv. Отдельный фактортип в Rocq при этом не строился — и не по нехватке, а сознательно (§ 3.4.3): глава работала с формализованным сетоидом и доказанным мостом, не реифицируя классы в новое типовое пространство точек.

Путь был такой. Сначала — почему точка не может быть первичной: готовая прямая из точек-атомов есть завершённая бесконечность, а её $P 4$ исключает; первичны процессы, точка должна быть из них построена (§ 3.2). Затем — отношение <<задавать одно число>>, cauchy_equiv, с доказанными рефлексивностью, симметричностью, транзитивностью — отношение, не сводящееся к поточечному равенству (§ 3.3); и доказанный в ProcessBridge.v мост, связывающий две репрезентации процесса в один объект (§ 3.3.1). Затем — определение: точка есть класс эквивалентности процессов, причём класс понимается как setoid-режим отождествления, а не завершённая совокупность, и фактортип отдельным Rocq-типом честно не строится (§ 3.4). Затем — точка как режим, а не объект: производный угол зрения на процессы, при котором виден предел и не виден способ (§ 3.5). Затем — арифметика на классах: сложение, отрицание и умножение доказанно спускаются на классы (cauchy_mul_Proper), а порядок спускается полностью (cauchy_le_compat) (§ 3.6). Наконец — разбор $0, 999 \dots = 1$ : два процесса, один класс, одно число, а <<парадокс>> — артефакт точечной картины; равенство доказано теоремой nine_equiv_one (§ 3.7).

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

{ Построенное в этой главе тоже имеет E/R/R-устройство (Часть I), и его разбор кристаллизует главный поворот главы. Заголовки опорных файлов задают разметку: ProcessCore.v объявляет правило — всякий объект есть конечный процесс на каждой стадии ( $P 4$ ); а отношение cauchy_equiv/process_equiv и мост ProcessBridge.v дают правило отождествления.³ Ведём разбор в онтологическом порядке Rules $\to$ Roles $\to$ Elements. Оговорка о статусе: всё ниже — содержательное чтение; фактортип отдельным Rocq-типом не построен (§ 3.4.3), и <<система>> здесь — не объект System $L$ .}

Rules — правила (закон $L 5$ ). Конституция та же, что в Главе 4.2, — принцип $P 4$ : число есть процесс, а не завершённая точка, и потому <<класс>> читается как setoid-режим, а не как завершённая совокупность (§ 3.4.2). Главное правило главы — отношение эквивалентности cauchy_equiv (<<задавать один предел>>, не поточечное равенство, § 3.3): именно оно отождествляет процессы. Его рефлексивность, симметричность, транзитивность делают факторизацию корректной (разбиение на непересекающиеся классы — математическое следствие этих трёх лемм). К нему примыкают правила согласованности: сложение и отрицание спускаются на классы (cauchy_add_compat, cauchy_neg_compat); порядок — лишь частично (cauchy_le_of_equiv, § 3.6.3); а мост ProcessBridge.v согласует две репрезентации процесса.

Roles — значимость позиций (закон $L 4$ ). Здесь — сам поворот главы, прочитанный как E/R/R. Точка — это роль, а не элемент. Она не предмет среди предметов, а режим рассмотрения процессов: класс эквивалентности, угол зрения, при котором эквивалентные процессы не различаются (§ 3.5). Это завершает прогрессию ролевых статусов Главы 4.2: кандидат $\to$ представитель $\to$ число (класс); число-точка — финальная роль, реализуемая правилом факторизации. По $L 4$ роль обоснована: класс есть структурный инвариант пучка эквивалентных процессов, а не произвольное их объединение.

Elements — носители (закон $L 1$ и принцип $P 4$ ). Элементы — процессы-представители (CauchySeq) и рациональные приближения под ними. Существенно: точка не есть элемент — первичны процессы, а точка из них производна (§ 3.2). По $L 1$ каждый процесс-представитель тождествен себе; по $P 4$ наблюдаем он конечными префиксами, а класс не собирается в завершённую совокупность.

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

Компонент	Что фиксирует	E/R/R
процессы-представители (`CauchySeq`); приближения	носители (точка — не элемент)	Element
точка $=$ класс $=$ режим отождествления	роль (производная)	Role
$P 4$ : число есть процесс, не точка	конституция	Rule
`cauchy_equiv` (refl/sym/trans)	правило отождествления	Rule (конкр.)
совместимость (`add_compat`); мост репрезентаций	согласованность	Rule (конкр.)
законы $L 1$ – $L 5$	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: процессы — элементы, точка-класс — роль, эквивалентность — правило. И здесь разбор оборачивается диагностикой: <<парадокс>> $0, 999 \dots = 1$ (§ 3.7) был смешением категорий — точку- роль (класс) принимали за элемент-объект и спрашивали, <<одна это точка или две>>. В верной разметке вопрос растворяется: два процесса-элемента, одна роль-класс. Это та самая диагностика парадоксов как смешения E/R/R-категорий, что введена в Части I.

Разбор продолжает E/R/R-фундамент Части IV (Глава 4.2). Если там процессное число было прочитано как прогрессия ролей, то здесь завершающая роль — точка как класс-режим — получает явный смысл: она не первичный элемент, а производная роль, заданная правилом cauchy_equiv над элементами-процессами. Как и множество в Частях I–II оказалось режимом, а не вещью, точка здесь оказывается режимом, а не атомом. Глава 4.4 спросит, сколько таких ролей-классов, — и счёт там пойдёт по классам.

Точка восстановлена на верном месте

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

{ Стоит сразу уточнить, в каком именно смысле точка <<построена>> — заголовок этого раздела силён, и его нужно прочесть точно. Точка построена в математико-онтологическом смысле: как setoid-класс эквивалентных представителей, как режим отождествления процессов по cauchy_equiv. В Rocq-ядре при этом построено не новое типовое пространство точек, а сетоид: отношение эквивалентности, зарегистрированное как Equivalence, с Proper-морфизмами операций (RealPointSetoid.v) — то, на чём чтение точки как класса и держится. Между двумя вещами глава всё время держала различие: точка как setoid-класс — построена и формализована; реифицированный фактортип отдельным Rocq-типом — сознательно не строится (§ 3.4.3, по $P 4$ ). }

$P 4$ -онтология, как видно, не обедняет математику. Привычные объекты — множество, точка, число — остаются; меняется лишь их порядок и статус. Первичны акты различения и процессы; множество и точка — производные режимы. Действительное число есть класс процессов; и эта картина не только не теряет ничего нужного, но и проясняет то, что в точечной картине оставалось тёмным, — как показал разбор $0, 999 \dots = 1$ .

Мост к Главе 4.4

Если точка есть класс процессов, немедленно встаёт вопрос о количестве. Сколько точек — то есть сколько классов? Процессов рациональных приближений необозримо много; классов, на которые cauchy_equiv их разбивает, — сколько? Счётно ли их множество, как у рациональных чисел, или несчётно?

Это предмет Главы 4.4. Она докажет несчётность — процессное прочтение классической теоремы Кантора. И здесь важно заранее указать две точности, прямо вытекающие из настоящей главы.

Первая — о том, что именно докажет следующая глава. Глава 4.4 не будет работать с уже построенным фактортипом точек: такого типа в репозитории нет, как установлено в § 3.4.3. Файл ProcessUncountable.v, на который она опирается, доказывает не теорему о фактортипе, а утверждение, равносильное несчётности для setoid-подхода: для всякого перечисления процессов найдётся процесс Коши (лежащий, в формулировке файла, в отрезке $[0, 1]$ ), не эквивалентный ни одному элементу перечисления. Иначе говоря, никакое перечисление представителей не покрывает все классы эквивалентности — всегда есть класс, в перечислении не представленный. Это и есть процессная несчётность: счёт идёт по классам, и счёта на все классы не хватает.

Вторая — о том, в каком смысле диагональный процесс <<отличается>> от перечисляемых. Он отличается по процессной эквивалентности: строится так, чтобы не попадать с перечисляемыми процессами в один класс — то есть не быть эквивалентным им по process_equiv. Это надо отличать от поточечного несовпадения. Поточечного несовпадения здесь недостаточно: два процесса могут различаться на каждом конечном шаге и всё равно задавать один класс (как десятичный процесс и единица в § 3.7); и наоборот, могут совпадать на бесконечно многих шагах, не будучи эквивалентными. Это просто разные свойства. Для диагонального аргумента Главы 4.4 нужно именно неэквивалентность по process_equiv, непопадание в общий класс, — и счёт там будет вестись по классам, как его подготовила настоящая глава.

{Итог главы — в трёх частях. Первое: что такое точка. Действительное число есть класс эквивалентности процессов рациональных приближений по отношению <<задавать один предел>>; точка — такой класс. Точка — не первичный атом прямой, а производный режим: процесс, взятый под углом, при котором виден предел и не виден способ к нему идти. <<Класс>> понимается как setoid-режим отождествления представителей, а не как завершённая совокупность.}

{Второе: что доказано формально. Отношение, по которому строится класс, — cauchy_equiv из CauchyReal.v на представителях CauchySeq; на голых процессах RealProcess ему отвечает process_equiv из ProcessCore.v — то же отношение общего предела на другой репрезентации, и мост между ними доказан в ProcessBridge.v. Отношение доказанно рефлексивно, симметрично и транзитивно (и зарегистрировано как Equivalence в RealPointSetoid.v). Сложение, отрицание и умножение классов доказанно корректны (cauchy_add_compat, cauchy_neg_compat, cauchy_mul_Proper); порядок тоже спускается на классы полностью (cauchy_le_compat).}

{Третье: что построено и что — сознательно нет. Переход к классам проведён на формализованном setoid-уровне (RealPointSetoid.v: Equivalence + Proper-морфизмы); реифицированный фактортип отдельным Rocq-типом не строится — по $P 4$ , не по нехватке (§ 3.4.3). На классы спущены сложение, отрицание, умножение и — полностью — порядок (cauchy_le_compat); деление частично, как и положено конструктивному полю. Равенство $0, 999 \dots = 1$ доказано теоремой nine_equiv_one (process/ProcessNinePoint.v, без аксиом): десятичный и постоянный процессы — разные представители одного класса, а <<парадокс>> был артефактом точечной картины. Сколько всего таких классов — счётно или несчётно — разбирает Глава 4.4.}

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

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

Навигация: ← Глава 2. RealProcess как тип · Глава 4. Несчётность процессов →

ProcessBridge.v Rocq-репозитория ToS (каталог src/process/), 10 доказанных утверждений, 0 Admitted, 0 аксиом. Заголовок файла: связать CauchySeq и RealProcess, сделав мост между ними явным. ↩
Эта частичность формализована как поле апартности. Отделённость от нуля — это предикат apart0 (предъявленный рациональный зазор $q < ∣ x ∣$ ), и теорема apart_has_inverse даёт: обратный по умножению существует в точности для апартных от нуля элементов; всё вместе — apartness_field. Так частичность деления — не дефект, а доказанная конструктивная структура. Машинно проверено, 6 Qed, 0 аксиом. ↩
E/R/R-разметка в шапках ProcessCore.v и ProcessBridge.v; здесь разворачивается по образцу Части I. ↩

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

Проводник