Глава 4. От позиции к процессу

Квадрат, равный двум

Где стоит Часть III

Часть III прошла долгий путь. Начав с натурального ряда, полученного в Части II, она развернула целые числа — двустороннюю координатную разметку (Глава III.1); рациональные числа — соразмерную разметку с дробным шагом (Глава III.2); и показала, что рациональные числа перечислимы (Глава III.3). На всём этом пути число понималось одним и тем же образом: как позиция — точка координатной разметки, взятая относительно опоры.

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

Диагональ единичного квадрата

Возьмём квадрат со стороной в одну единицу и проведём в нём диагональ. Спросим: какова длина этой диагонали?

Вопрос законный и древний. Диагональ — вполне определённый отрезок; у неё есть длина, её можно отложить на координатной разметке. По теореме, известной задолго до всякой теории чисел, квадрат длины диагонали равен сумме квадратов сторон: $1+1$, то есть $2$. Длина диагонали есть, стало быть, такое число, которое, взятое дважды сомножителем, даёт $2$.

Обозначим искомое число $r$ и запишем условие, которому оно должно отвечать:

$$r\cdot r=2.$$

Задача поставлена. Есть отрезок — диагональ единичного квадрата; есть условие на его длину — $r\cdot r=2$. Остаётся спросить: какая позиция соразмерной разметки этому условию отвечает?

Вопрос, который предстоит разобрать

Соразмерная разметка плотна (Глава III.2): между всякими двумя позициями лежит ещё одна, разметка сгущается без предела. Естественно ждать, что среди этого густого множества позиций найдётся и та, чей квадрат равен двум: ведь позиции подходят, кажется, к всякому месту сколь угодно близко.

Так вот: такой позиции нет. Ни одно рациональное число не даёт в квадрате двойку. Это — не предположение, а доказанный факт, и Часть III докажет его строго в следующем разделе. Но прежде стоит сказать прямо, чего этот факт не означает, — чтобы не прочесть его превратно.

Он не означает, что в соразмерной разметке есть изъян, прореха, что рациональные числа в чём-то ущербны. Часть III построила их как полноценную систему — упорядоченную, плотную соразмерную разметку, чья стандартная алгебраическая роль есть роль поля и которая показана счётной явным обходом, — и ничего из этого не отменяется. Он означает иное: что условие $r\cdot r=2$ есть условие особого рода — такое, какое ни одна позиция выполнить не может. И встреча с таким условием не обрывает путь Части III, а поворачивает его: за условием, которое позиции не по силам, разворачивается число иного рода. Какое — глава покажет, пройдя сперва само доказательство.

Ни одна дробь не даёт двойку

Что нужно доказать

Утверждение, к которому подошла предыдущая глава, таково: ни одно рациональное число, взятое дважды сомножителем, не даёт двойки. На языке дробей: нет такой дроби $p/q$, чтобы $(p/q)\cdot (p/q)$ равнялось $2$.

Дробь $p/q$ даёт в квадрате $p^2/q^2$. Условие $(p/q{)}^2=2$ значит, стало быть, $p^2/q^2=2$, а это — что $p^2=2q^2$. Доказать нужно, выходит, следующее: не существует целых чисел $p$ и $q$, $q$ не равно нулю, для которых $p^2=2q^2$. Стоит сразу оговорить техническую подробность записи. В стандартной записи рационального числа Rocq числитель есть целое, а знаменатель положителен по устройству типа (тип positive, Глава III.2, § 2.5). Поэтому доказательство строится в два приёма: сперва доказывается промежуточная теорема для произвольных целых $p$ и $q$ при условии $q\ne 0$, а затем она применяется к рациональному числу, у которого знаменатель имеет вид $q=‘Z.pos‘(d)$ с положительным $d$. Доказанное и установит, что условие $r\cdot r=2$ не выполнимо ни одной рациональной позицией.

ToS доказывает это строго и конструктивно.¹ Доказательство ведётся приёмом, который называют бесконечным спуском, и приём этот стоит пройти, ибо он сам по себе поучителен.

Чётность числа и чётность его квадрата

Доказательство опирается на одно простое наблюдение о чётности.

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

Это наблюдение — рычаг всего доказательства. Из него выводится ключевой шаг: если $p^2=2q^2$, то $p$ и $q$ оба чётны. Разберём почему. Равенство $p^2=2q^2$ говорит, что $p^2$ есть удвоенное нечто, — значит, $p^2$ чётно, а тогда по наблюдению чётно и $p$. Раз $p$ чётно, оно есть удвоенное некоторое целое: $p=2k$. Подставим: $(2k{)}^2=2q^2$, то есть $4k^2=2q^2$, откуда $q^2=2k^2$. Но это значит, что и $q^2$ чётно, — а тогда чётно и $q$. Итак, из $p^2=2q^2$ следует, что $p$ и $q$ оба чётны.³

Бесконечный спуск

Теперь приём спуска. Пусть нашлись целые $p$ и $q$, для которых $p^2=2q^2$. Только что показано: оба они чётны, $p=2p^{\prime }$ и $q=2q^{\prime }$. Подставим в равенство и сократим: $(2p^{\prime }{)}^2=2(2q^{\prime }{)}^2$ даёт $4p^{\prime 2}=8q^{\prime 2}$, то есть $p^{\prime 2}=2q^{\prime 2}$. Половинки $p^{\prime }$ и $q^{\prime }$ удовлетворяют тому же самому равенству.⁴

Но тогда и $p^{\prime }$, $q^{\prime }$ оба чётны — по тому же доводу, — и делятся пополам, давая $p»$ и $q»$, опять с тем же равенством. И снова. И снова. Спуск не кончается: всякая пара решений порождает пару вдвое меньших, и так без предела.

Здесь — противоречие, и стоит назвать его точно, как оно проведено в формализации. Возьмём меру пары решений — сумму $|p|+|q|$, неотрицательное целое число. Всякий шаг спуска эту меру строго уменьшает: половинки $p^{\prime }$, $q^{\prime }$ имеют сумму модулей вдвое меньшую. Но цепочка строго убывающих неотрицательных целых не может быть бесконечной — всякая такая цепочка обрывается. Формально это и есть сильная индукция по мере $|p|+|q|$: предполагая утверждение доказанным для всех пар с меньшей мерой, его доказывают для пары с данной мерой, а единственная пара, у которой спуск не может уменьшить меру (ибо мера уже наименьшая, нулевая), — это пара нулей $p=0$, $q=0$. Так Rocq избегает неформального рассуждения о <<бесконечном процессе деления>>: вместо ссылки на <<бесконечный спуск>> как таковой доказательство опирается на строгий принцип — сильную индукцию по убывающей целочисленной мере. Вывод: всякое решение $p^2=2q^2$ есть пара нулей.⁵ А пара нулей условию задачи не отвечает: знаменатель $q$ дроби нулём быть не может (Глава III.2, § 2.4). Значит, ни одна дробь условию $p^2=2q^2$ не удовлетворяет.

Ни одно рациональное число не даёт в квадрате двойки. Если бы дробь $p/q$ удовлетворяла $p^2=2q^2$, то $p$ и $q$ были бы оба чётны, их половины удовлетворяли бы тому же равенству, и так без конца. Формально это противоречие проводится сильной индукцией по мере $|p|+|q|$: каждый шаг спуска строго уменьшает эту меру, а строго убывающая цепь неотрицательных целых не может быть бесконечной, — и единственное решение есть пара нулей. Но нуль не может быть знаменателем. ToS доказывает это конструктивно, без единой аксиомы и без закона исключённого третьего.

Как читать этот результат

Итог доказан; теперь важно прочесть его верно, ибо здесь легче всего сбиться.

Доказанное — утверждение отрицательное по форме: нет такой дроби. И велик соблазн прочесть его как весть об ущербе: будто в соразмерной разметке обнаружилась прореха, будто рациональным числам чего-то недостаёт. Это было бы неверно. Доказательство не нашло в $Q$ изъяна. Оно установило точный факт о позициях: условие $r\cdot r=2$ не выполняется ни одной позицией соразмерной разметки.

И вопрос, который из этого встаёт, — не <<чем залатать разметку>>, а совсем другой: если условие $r\cdot r=2$ не по силам никакой позиции — то какому объекту оно по силам? Ведь диагональ единичного квадрата есть, длина у неё есть, и условие на эту длину поставлено законно. Объект, отвечающий условию, должен быть — но он не позиция. Что же он такое? К этому вопросу глава переходит, и ответ на него составляет её существо.

Роль, которую не несёт позиция

Условие есть, объекта-позиции нет

Предыдущий раздел оставил глава с точно очерченным положением дел. Есть условие — $r\cdot r=2$. Есть отрезок, к которому оно относится, — диагональ единичного квадрата. И доказано: ни одна позиция соразмерной разметки этому условию не отвечает.

Положение это легко прочесть как тупик — но тупик был бы лишь в одном случае: если бы всякий математический объект был позицией. Тогда <<нет позиции>> значило бы <<нет объекта>>, и путь обрывался бы. Но с чего бы всякому объекту быть позицией? Часть III работала с числом-позицией, потому что разворачивала координатную разметку, и для разметки позиция — естественный и достаточный род объекта. Это не значит, что иных родов нет. Доказанное в § 4.2 не говорит <<объекта нет>>; оно говорит точнее: объект, отвечающий условию $r\cdot r=2$, не есть позиция. А каков он — вопрос открытый, и глава на него ответит.

Позиция и уровень рассмотрения

Чтобы ответить, нужно вернуться к различению, введённому в Части I, — к различению уровней рассмотрения.

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

Приложим это к числам. Рациональное число — позиция соразмерной разметки — есть элемент. На уровне разметки оно простое: точка, взятая относительно опоры, без внутреннего устройства, потребного для разметки. Часть III работала именно на этом уровне — на уровне рациональных чисел как элементов. И доказанное в § 4.2 есть факт об этом уровне: на уровне элементов-позиций условие $r\cdot r=2$ не выполняется.

Но из того, что условие не выполняется на уровне элементов, не следует, что оно не выполняется вовсе. Оно может выполняться на уровне выше — на уровне систем, составленных из этих элементов. И глава покажет, что именно так и есть: условие $r\cdot r=2$ выполняется не элементом, а системой из элементов — объектом следующего уровня.

Роль как принадлежность уровню

Сказанное стоит уточнить в терминах роли — одного из трёх понятий, какими Часть I описывала строение системы.

<<Давать в квадрате двойку>> — это роль. Роль — не сам объект, а то, что объект делает, чем он служит, какое условие выполняет. И всякая роль принадлежит некоторому уровню: есть роли, посильные элементу, и роли, посильные лишь системе. Целое число в роли позиции на двусторонней разметке, рациональное в роли позиции на соразмерной — это роли, посильные элементу: элемент с ними справляется, и уровня выше не требуется.

Роль <<давать в квадрате двойку>> элементу не посильна — это и доказал § 4.2. Скажем это точнее, чтобы слово <<роль>> не прозвучало слишком расплывчато. Условие $r\cdot r=2$ есть предикат на рациональных позициях — свойство, которое позиция либо несёт, либо нет; и доказанное в § 4.2 говорит ровно то, что этот предикат пуст на $Q$: ни один элемент типа $Q$ его не выполняет. Формально это и есть теорема sqrt2_not_in_Q файла Sqrt2Irrational.v: не существует рационального $r$, для которого $r\cdot r$ равно $2$.⁶ Но из того, что предикат пуст на уровне элементов-позиций, не следует <<роль невыполнима вовсе>>, а следует <<роль принадлежит другому уровню>>. Её носитель — не элемент, а система: объект, составленный из рациональных элементов, связанных ролями и правилом. Что это за система и как она устроена — глава покажет в следующем разделе, разобрав её прямо, по составу.

Из того, что условие $r\cdot r=2$ не выполняется ни одной позицией, не следует, что оно не выполняется вовсе. Рациональное число — позиция — есть элемент: простое на уровне разметки. Часть III работала на уровне элементов, и § 4.2 есть факт об этом уровне. <<Давать в квадрате двойку>> есть роль, и роль эта элементу не посильна — но посильна системе, объекту уровня выше, составленному из рациональных элементов. Условие выполняется не позицией, а системой из позиций.

К разбору системы

Итак, объект, отвечающий условию $r\cdot r=2$, — система, составленная из рациональных чисел. Назвать её одним словом — значит назвать процесс. Следующий раздел разберёт этот процесс прямо: из чего он состоит, какими ролями связаны его составляющие и каким правилом он держится.

Корень из двух как процесс

Классическое имя и то, что за ним

Объект, отвечающий условию $r\cdot r=2$, классическая математика называет квадратным корнем из двух и записывает $\sqrt{2}$. Записывают его и десятичной дробью — $1,41421\dots$ — с многоточием, отсылающим к бесконечному, никогда не выписываемому до конца хвосту цифр.

ToS принимает имя $\sqrt{2}$, но спрашивает, что за ним стоит. И здесь её ответ расходится с привычным. Привычно $\sqrt{2}$ мыслят как одно число — единый объект-позицию, который где-то <<есть>>, а десятичная запись лишь приближённо его называет. ToS видит иначе: $\sqrt{2}$ есть не одна числовая позиция, а процесс — развёртывающаяся последовательность рациональных приближений. ToS не спорит с тем, что в стандартной математике $\sqrt{2}$ есть вещественное число; она говорит, что само вещественное число будет понято как процесс. И этот процесс, в отличие от <<одной позиции>>, можно разобрать по составу — что глава и делает.

Процесс уточняющихся приближений

Возьмём конкретный процесс, дающий $\sqrt{2}$.⁷ Начнём с грубого рационального приближения — скажем, с единицы. И зададим правило, которое из всякого приближения делает приближение точнее: если $x$ — текущее приближение, то

$$x^{\prime }=\frac{x+2/x}{2}$$

есть приближение следующее. Правило это — усреднение $x$ с числом $2/x$ — известно как итерация Ньютона. Применяя его раз за разом, получаем ряд рациональных чисел:

$$1,\frac{3}{2},\frac{17}{12},\frac{577}{408},\dots$$

Каждый член ряда есть рациональное число — наличная позиция соразмерной разметки, конечный объём данных. На первых шагах видно, как процесс резко уточняет приближение: квадрат первого члена есть $1$, второго — $9/4$, третьего — $289/144$, и третий уже отстоит от двойки на $1/144$. Здесь нужна, однако, точность относительно того, что именно доказано. Файл RefinementSqrt.v доказывает конкретные значения первых членов и сравнивает качество приближения на шаге $2$; но утверждение, что каждый следующий шаг строго точнее предыдущего, и утверждение о сходимости процесса в этом файле не доказаны как теоремы. Поэтому глава говорит осторожно: на первых шагах резкое уточнение видно прямым вычислением, а для полного утверждения о монотонном улучшении и о сходимости требуется отдельная теорема о данном процессе (§ 4.5).

Чтобы сказать <<процесс даёт $\sqrt{2}$>> строго — и сказать это, не ссылаясь на $\sqrt{2}$ как на уже готовую точку, — введём предикат на процессах. Процесс $R:N\to Q$ даёт $\sqrt{2}$, если выполнены два условия: во-первых, $R$ есть процесс Коши (его члены неограниченно сближаются между собой); во-вторых, его квадратичная погрешность $|R(n)\cdot R(n)-2|$ становится меньше всякой наперёд заданной точности. Формально:

$$\mathrm{sqrt}{2}_{\mathrm{p}}\mathrm{rocess}(R):=\mathrm{i}{\mathrm{s}}_{\mathrm{C}}\mathrm{auchy}(R)\wedge \forall \epsilon >0\exists N\forall n\ge N:|R(n)\cdot R(n)-2|<\epsilon .$$

Так $\sqrt{2}$ задаётся не как готовая точка, к которой что-то стремится, а как предикат на процессах — условие, которому процесс рациональных приближений отвечает или не отвечает. Стоит сразу сказать и о статусе этого предиката в репозитории: само определение sqrt2_process есть естественная формализация, но теоремы вида <<sqrt2_newton удовлетворяет sqrt2_process>> в текущем виде RefinementSqrt.v ещё не доказаны; глава вводит этот предикат как точную формулировку, к которой формализация должна прийти, а не как уже доказанный факт.

Вот этот разворачивающийся ряд приближений и есть один из процессов, дающих $\sqrt{2}$. Не точка, к которой ряд <<стремится>> и которая лежит где-то отдельно от него готовой, — а сам ряд, само развёртывание. $\sqrt{2}$ даётся процессом — и таких процессов, как покажет § 4.5, не один.

Корень из двух как функциональная система

Процесс, дающий $\sqrt{2}$, — это процесс, и ToS разбирает его точным языком, языком функциональной системы, введённым в Части I. Всякая функциональная система раскладывается на три слоя — правила, роли и элементы. Сперва разложим на эти три слоя $\sqrt{2}$, чтобы увидеть систему целиком; затем разберём каждый слой по порядку.

Разложение даёт общую картину. Правила системы $\sqrt{2}$ — это закон, по которому она разворачивается, и критерий, которому она подчинена. Роли — это то, чем служит в системе всякая её составляющая. Элементы — это сами составляющие, наличные рациональные числа. Три слоя — и $\sqrt{2}$ предстаёт как система, имеющая задачу, имеющая ролевое устройство, имеющая материал. Теперь разберём слои по порядку, начиная с правил: ибо правила суть задача системы, а понять систему значит прежде всего понять, ради чего она.

Правила. Правила — конституция системы $\sqrt{2}$, и с них разбор начинается, ибо они задают, что система делает. Правил здесь два. Первое — правило сходимости: требование, чтобы приближения неограниченно сближались, чтобы погрешность убывала к нулю. Это и есть задача системы $\sqrt{2}$ — сходиться, и сходиться к тому, чей квадрат есть двойка. Второе — правило порождения: формула $x^{\prime }=(x+2/x)/2$, по которой из всякого приближения строится следующее. Первое правило задаёт, к чему система идёт; второе — как она шаг за шагом идёт. Вместе они суть конституция: $\sqrt{2}$ есть та система, чьё дело — сходиться по этому закону к этому пределу.

Роли. Раз задача системы — сходиться, всякая её составляющая получает определённую этой задачей роль: быть приближением такого-то качества. Роль не привходит к составляющей извне — она конституируется правилом: коль скоро правило задаёт критерий сходимости, всякая составляющая занимает по отношению к этому критерию своё место, и место это есть её роль. Качество измеряется прямо: насколько квадрат приближения близок к двойке. Приближение $17/12$ даёт в квадрате $289/144$, что отстоит от двойки на $1/144$, — и играет роль <<приближение с погрешностью $1/144$>>. Следующее приближение играет роль более точного, ещё следующее — ещё более точного. Роль составляющей есть её качество как приближения, и ToS измеряет это качество явной величиной — модулем разности квадрата и двойки.⁸

Элементы. Наконец, элементы — то, что эти роли несёт. Элементы системы $\sqrt{2}$ суть рациональные приближения: $1$, $3/2$, $17/12$, $577/408$ и так далее. Каждое из них есть наличное рациональное число, позиция соразмерной разметки, построенная Частью III. Элементы стоят в разборе последними не по малозначности — без них системе не из чего быть, — а потому, что определяются они ролью: рациональное число входит в систему $\sqrt{2}$ постольку, поскольку несёт роль приближения, а роль эта задана правилом. Система $\sqrt{2}$ не вводит новых, неведомых сущностей: её элементы — рациональные числа, уже имеющиеся. $\sqrt{2}$ как процесс не является рациональной позицией — это доказано (§ 4.2), — но все его стадии вполне рациональны. Он не добавляет к разметке нового рационального элемента; он задаёт систему, составленную из рациональных элементов и связывающую их ролями под единым правилом.

Правила, роли, элементы — разобранный процесс есть функциональная система, описанная по всем трём слоям. И описана она полностью: ничего, кроме двух правил, ролевого качества и рациональных приближений, для неё не нужно. Таков один процесс, дающий $\sqrt{2}$; следующий раздел покажет, что он не единствен. (Свод этого разбора в таблицу и проверку сформированности системы даёт § 4.8.2.)

Корень из двух существует позитивно

Теперь видно, в чём ошибочна привычная картина $\sqrt{2}$ как <<недостающего числа>> — и почему ToS её отвергает.

Назвать $\sqrt{2}$ недостающим, прорехой, тем, чего рациональным числам не хватает, — значит определить его через отсутствие, взглядом со стороны рациональных чисел: $\sqrt{2}$ как <<то, чего там нет>>. Но так $\sqrt{2}$ вообще не определено — так очерчена лишь граница рациональных чисел, а не сам $\sqrt{2}$. ToS определяет $\sqrt{2}$ через то, что есть: есть элементы — наличные рациональные приближения; есть роли — их качества; есть правила — порождение и сходимость. $\sqrt{2}$ существует позитивно, как функциональная система: не отсутствием на уровне рациональных чисел, а присутствием на уровне выше — на уровне систем, составленных из рациональных чисел.

Это снимает кажущийся тупик § 4.2 совершенно. Условие $r\cdot r=2$ не выполняется позицией — верно; но оно выполняется системой. Рациональные числа — элементы, простое; процесс, дающий $\sqrt{2}$, — система из этих элементов, целое уровнем выше. Не <<в разметке прореха>>, а <<над разметкой — система>>. Часть III не упёрлась в изъян; она дошла до уровня элементов и тем самым подвела к уровню систем.

$\sqrt{2}$ есть не одно число-позиция в $Q$, а процесс рациональных приближений. Процесс этот — функциональная система, описанная тремя слоями: её элементы суть рациональные приближения ($1$, $3/2$, $17/12$, $\dots$), наличные позиции соразмерной разметки; её роли — качество приближения, измеряемое близостью квадрата к двойке; её правила — порождение (формула следующего приближения) и сходимость (убывание погрешности к нулю). $\sqrt{2}$ существует позитивно: не отсутствием на уровне рациональных чисел, а присутствием на уровне систем, из рациональных чисел составленных.

К множественности процессов

Глава разобрала один процесс, дающий $\sqrt{2}$, — ньютонов. Но он не единственный. $\sqrt{2}$ даётся и иными процессами, устроенными иначе, — и сравнение их между собой проясняет природу числа-процесса ещё точнее. К этому глава переходит в следующем разделе.

Процессов много

Не один процесс, а класс процессов

Глава разобрала $\sqrt{2}$ как процесс — как функциональную систему уточняющихся приближений. Но разобран был один процесс, ньютонов. Стоит спросить: единствен ли он? Есть ли у $\sqrt{2}$ один этот процесс — или их несколько?

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

Второй процесс: цепная дробь

Наряду с ньютоновым $\sqrt{2}$ даётся процессом цепной дроби.⁹ Устроен он иначе. Ньютонов процесс порождал каждое приближение усреднением; процесс цепной дроби строит приближения по своему правилу — через пары числителей и знаменателей, нарастающих особой рекурренцией. Правило иное — и ряд приближений иной:

$$1,\frac{3}{2},\frac{7}{5},\frac{17}{12},\dots$$

Это — другой процесс. Другое правило порождения, другие элементы: другие рациональные приближения встают в ряд.

Сравним два ряда. Ньютонов процесс даёт

$$1,\frac{3}{2},\frac{17}{12},\frac{577}{408},\dots$$

процесс цепной дроби —

$$1,\frac{3}{2},\frac{7}{5},\frac{17}{12},\dots$$

На первом шаге оба дают $1$; на втором — оба дают $3/2$; процессы совпадают.¹⁰ Но на третьем шаге они расходятся: ньютонов даёт $17/12$, процесс цепной дроби — $7/5$. Это разные рациональные числа, и ToS отмечает их различие отдельной теоремой.¹¹ Два процесса, совпав на первых шагах, дальше идут разными путями.

Процессы сравнимы по качеству

Раз процессов несколько и на одном шаге они дают разные приближения, естественно спросить: какое из приближений лучше? И вопрос этот имеет точный ответ, ибо качество приближения ToS измеряет явной величиной (§ 4.4).

На третьем шаге ньютонов процесс даёт $17/12$, процесс цепной дроби — $7/5$. Качество $17/12$ есть $|(17/12{)}^2-2|=1/144$; качество $7/5$ есть $|(7/5{)}^2-2|=1/25$. Величина $1/144$ меньше $1/25$ — значит, ньютоново приближение на этом шаге точнее: его квадрат ближе к двойке. ToS доказывает это сравнение теоремой.¹²

Два процесса, стало быть, не просто различны — их приближения можно сравнивать по явной функции качества. И здесь снова нужна точность относительно доказанного. В файле RefinementSqrt.v формально проверено конкретное сравнение — на шаге $2$: ньютоново приближение там точнее цепно-дробного. Общее же утверждение — что на всяком шаге одно приближение сравнимо с другим и можно сказать, какое ближе к цели, — этим файлом не доказано; оно потребовало бы отдельной теоремы. Стоит добавить и оговорку о самом слове <<сравнимы>>: качества двух приближений сравнимы отношением $\le$ — но если на каком-то шаге качества равны, сказать, <<какое лучше>>, нельзя, можно лишь констатировать равенство. Точная формулировка такова: приближения процессов сопоставимы по явной мере качества, и одно конкретное сравнение, на шаге $2$, в репозитории доказано.

Что множественность процессов проясняет

Множественность процессов проясняет природу $\sqrt{2}$ и окончательно снимает остатки картины <<недостающего числа>>.

Если бы $\sqrt{2}$ было одной точкой, одним недостающим числом, то говорить о <<разных $\sqrt{2}$>> было бы бессмысленно: точка одна, и все пути к ней лишь по-разному её нащупывают. Но $\sqrt{2}$ — не точка, а процесс, и процессов вправду несколько: ньютонов и цепной дроби суть разные системы — разные правила, разные элементы, разное качество на каждом шаге. Они не <<приближают одно и то же заранее данное число>> — они суть разные способы развернуть $\sqrt{2}$.

Здесь нужно точно сказать, в каком смысле эти разные процессы дают одно и то же $\sqrt{2}$. Не в том смысле, что они равны как процессы: равенство процессов <<по шагам>> (в репозитории — отношение process_eq файла ProcessRefinement.v, требующее совпадения на каждом шаге) для них не выполняется — они расходятся уже на третьем шаге. Их единство задаётся не пошаговым равенством, а более слабым отношением — отношением эквивалентности процессов: два процесса эквивалентны, если их взаимное расстояние становится меньше всякой наперёд заданной точности — если $|R(n)-S(n)|$ уходит к нулю. Такое отношение в репозитории уже есть — это process_equiv файла ProcessCore.v, определённое как

$$\mathrm{proces}{\mathrm{s}}_{\mathrm{e}}\mathrm{quiv}(R,S):=\forall \epsilon >0\exists N\forall n\ge N:|R(n)-S(n)|<\epsilon ,$$

и для него там доказаны рефлексивность, симметрия и транзитивность — то есть это настоящее отношение эквивалентности.¹³ И тогда $\sqrt{2}$, в процессном чтении ToS, есть не отдельная рациональная позиция и не один выделенный процесс, а класс эквивалентных процессов рациональных приближений — класс всех процессов, удовлетворяющих условию $\mathrm{sqrt}{2}_{\mathrm{p}}\mathrm{rocess}$ (§ 4.4) и эквивалентных между собой по process_equiv.

Двух разобранных процессов довольно, чтобы увидеть неединственность, — но стоит точно сказать, что здесь показано, а что намечено. Формально в файле RefinementSqrt.v построены и сопоставлены два конкретных процесса — ньютонов и цепной дроби — и доказано их различие на шаге $2$. Уже этих двух довольно, чтобы утверждать: процессное представление $\sqrt{2}$ не единственно. Более сильное утверждение — что таких процессов открытое семейство — естественно и математически стандартно, но в текущем виде репозитория оно не формализовано, и глава приводит его как содержательную программу, а не как доказанный факт. Содержательно основания для него таковы: ньютоново правило $x^{\prime }=(x+2/x)/2$ применимо к любому начальному рациональному приближению (глава начала с единицы, но можно начать с $3/2$, с $2$, с иной разумной дроби — и всякий выбор начала даёт свой процесс с тем же правилом), а помимо ньютонова правила и правила цепной дроби есть и иные правила уточнения. Полная формализация открытого семейства потребовала бы, например, параметризованных ньютоновых процессов с разными начальными приближениями и доказательства их сходимости.

И ещё одна оговорка о словах. Говоря о совокупности процессов, дающих $\sqrt{2}$, глава пользуется словами класс, семейство, схема — но не словом множество в смысле завершённой, готовой совокупности. Это согласовано с принципом $P4$: ToS не берёт совокупность всех процессов как completed totality, как готовое собранное целое. $\sqrt{2}$ есть не завершённое множество всех своих процессов, а открытая схема процессов, задаваемых правилами уточнения, — открытый класс эквивалентных рациональных процессов.

Здесь видно, до чего обманчива была бы метафора прорехи. Прореха — это одно пустое место, нехватка, отсутствие. А на деле на месте $\sqrt{2}$ — не отсутствие, а обилие: множество процессов, и каждый есть полноценная функциональная система с правилами, ролями, элементами, и все они сравнимы между собой. Там, где привычная картина видела пустоту, ToS обнаруживает богато устроенную область — семейство процессов. Не нехватки, а избытка.

$\sqrt{2}$ даётся не одним процессом, а классом процессов. Наряду с ньютоновым его даёт процесс цепной дроби — с иным правилом порождения и иными приближениями ($1,3/2,7/5,17/12,\dots$). Два процесса совпадают на первых шагах и расходятся дальше; одно сравнение их качества, на шаге $2$, в репозитории доказано. Разные процессы дают одно $\sqrt{2}$ не потому, что равны по шагам, а потому, что эквивалентны — их взаимное расстояние уходит к нулю (process_equiv). $\sqrt{2}$ есть, стало быть, не точка и не один процесс, а открытый класс эквивалентных сходящихся процессов. Метафора прорехи обманчива: на месте $\sqrt{2}$ — не отсутствие, а обилие.

К достижимости приближений

Глава показала, что $\sqrt{2}$ даётся процессом и что таких процессов открытый класс. Среди правил процесса (§ 4.4) было правило сходимости — требование, чтобы погрешность убывала к нулю. Само требование установлено; но выполнимо ли оно — зависит от устройства рациональных чисел. То свойство их устройства, которое делает правило сходимости выполнимым, разбирает следующий раздел.

Приближение достижимо: архимедово свойство

Чего требует правило сходимости

Разбирая $\sqrt{2}$ как функциональную систему (§ 4.4), глава назвала среди её правил правило сходимости: требование, чтобы погрешность приближений убывала к нулю. Правило это уже установлено — оно часть конституции системы. Спросим теперь, что в устройстве рациональных чисел делает его выполнимым.

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

Так вот: рациональные числа устроены так, что правило сходимости выполнимо. Что именно в их устройстве это обеспечивает — имеет точное имя: архимедово свойство. Глава не вводит его как новое допущение и не проверяет задним числом скрытую посылку — она указывает в уже построенном (Глава III.2) то свойство рациональных чисел, которое подходит под правило сходимости и делает его выполнимым.

Архимедово свойство

Архимедово свойство в той форме, в какой оно нужно процессам уточнения, говорит о делении пополам.

Возьмём дробь $1/2$, затем половину её — $1/4$, затем половину половины — $1/8$, и так далее: $1/2$, $1/4$, $1/8$, $1/16$, $\dots$ — доли, убывающие вдвое на каждом шаге. Архимедово свойство утверждает: какую угодно малую точность ни задай, в этом ряду половинных долей найдётся доля ещё меньшая. Сколь бы тесную меру $\epsilon$ мы ни взяли, есть такое число шагов $N$, что доля $1/2^N$ уже меньше $\epsilon$.

ToS доказывает это строго.¹⁴ В основе доказательства — то, что степени двойки растут неограниченно: $2^N$ рано или поздно превзойдёт всякое наперёд заданное число, а значит, обратная величина $1/2^N$ станет меньше всякой наперёд заданной доли. Растут степени двойки не по допущению, а по доказанной лемме: ToS выводит их неограниченный рост из устройства самих натуральных чисел.

Достижимость как свойство процесса

Стоит вчитаться, о чём именно говорит архимедово свойство, — ибо говорит оно о процессе, и говорит на языке ToS.

Архимедово свойство не утверждает, что существует некая <<бесконечно малая>> величина или что ряд половинных долей <<доходит до нуля>>. Оно утверждает иное и более скромное: для всякой заданной точности процесс деления пополам достигает её за конечное число шагов. Не <<есть завершённая бесконечность долей>>, а <<есть процедура, и она доходит>>: задай точность — процедура назовёт шаг $N$, на котором эта точность взята. Это — то же операциональное понимание, каким Глава III.3 наделила счётность: не свойство готовой совокупности, а свойство работающей процедуры.¹⁵

И вот что архимедово свойство даёт процессам из § 4.4 и § 4.5 — но здесь нужна точность, чтобы не сказать больше доказанного. Архимедово свойство само по себе не доказывает сходимость каждого конкретного процесса. Оно доставляет общий инструмент: обеспечивает достижимость сколь угодно малых рациональных мер — для всякой точности находится шаг, на котором доля $1/2^N$ уже меньше её. Чтобы этот инструмент ручался за конкретный процесс, нужно ещё одно: для процесса должна быть получена оценка погрешности через убывающие доли — скажем, оценка вида $C/2^N$ или через ширину сжимающихся интервалов. Если такая оценка для процесса доказана, тогда архимедово свойство, приложенное к ней, и обеспечивает достижение любой точности. Само же по себе, без оценки погрешности конкретного процесса, архимедово свойство сходимости этого процесса не даёт. Так, файл Archimedean_ERR.v доказывает не только Archimedean, но и Archimedean_width (достижимость для масштабированной ширины) и shrinking_interval_Cauchy — теорему о том, что процесс, удерживаемый в интервалах с убывающей шириной, есть процесс Коши; и вот связка <<оценка ширины $+$ архимедово свойство>> уже ручается за сходимость. Сходимость, о которой глава говорила как о правиле процесса (§ 4.4), оказывается, стало быть, требованием выполнимым — но выполнимым через оценку погрешности, к которой архимедово свойство прилагается, а не через одно лишь архимедово свойство.

Правило сходимости (§ 4.4) требует, чтобы погрешность приближений убывала к нулю; выполнимо ли это требование — зависит от устройства рациональных чисел. То свойство их устройства, которое делает правило выполнимым, есть архимедово свойство: для всякой наперёд заданной точности $\epsilon$ найдётся шаг $N$, на котором доля $1/2^N$ уже меньше $\epsilon$. ToS его доказывает. Свойство это говорит о процессе: не <<есть завершённая бесконечность долей>>, а <<процедура деления пополам достигает всякой точности за конечное число шагов>>. Само по себе оно сходимости конкретного процесса не доказывает — оно даёт инструмент: приложенное к оценке погрешности процесса (через убывающие доли или ширину сжимающихся интервалов), оно и ручается, что процесс доходит до любой точности.

К сходимости процесса

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

Сжимающиеся интервалы: процесс есть Коши

Внутренняя сходимость процесса

Архимедово свойство (§ 4.6) ручается, что процесс достигает любой отдельно взятой точности. Но процесс есть не набор разрозненных достижений, а единое движение, и сходимость его — не только в том, что он подходит к цели. Сходимость процесса есть прежде всего его внутреннее свойство: его собственные приближения, взятые на достаточно далёких шагах, сближаются между собой.

Различие тонкое, но существенное. Можно говорить о сходимости, указуя на цель: приближения подходят к $\sqrt{2}$. Но цель — $\sqrt{2}$ — сама есть процесс, и определять сходимость процесса через приближение к процессу значило бы ходить по кругу. ToS определяет сходимость изнутри, не ссылаясь на цель: процесс сходится, если его собственные члены неограниченно сближаются друг с другом. Это и есть свойство, называемое свойством Коши.

Процесс Коши

Свойство Коши ToS определяет точно.¹⁶ Процесс есть процесс Коши, если для всякой наперёд заданной точности $\epsilon$ найдётся такой шаг $N$, что любые два приближения, взятые после него, отстоят друг от друга меньше чем на $\epsilon$. Не <<приближения подходят к цели>>, а <<приближения, начиная с некоторого шага, теснятся друг к другу теснее всякой наперёд заданной меры>>.

Определение это — операциональное, в том же смысле, в каком операциональны счётность (Глава III.3) и архимедово свойство (§ 4.6). Оно не говорит о завершённой бесконечности, не указывает на готовый предел. Оно описывает поведение процесса: задай меру $\epsilon$ — и процесс укажет шаг, после которого все его члены умещаются в эту меру по взаимному расстоянию. Свойство Коши есть характеристика поведения, а не данных, — и в этом оно под стать самому процессу, который тоже есть поведение, а не данные (Глава III.3, § 3.7).

Сжимающиеся интервалы

Откуда у процесса, дающего $\sqrt{2}$, берётся свойство Коши? Из того, как такой процесс устроен, — из механизма сжимающихся интервалов.

Механизм таков. Возьмём отрезок, о котором известно, что искомое — то, к чему процесс идёт, — лежит внутри него. Разделим отрезок и оставим ту половину, внутри которой искомое по-прежнему лежит. С нею поступим так же: разделим, оставим нужную половину. Шаг за шагом — вложенные отрезки, и каждый вдвое короче предыдущего: ширина их убывает $1,1/2,1/4,1/8,\dots$ — то есть убывает так, как половинные доли из § 4.6.

И вот связь с архимедовым свойством. Все приближения процесса, начиная с шага $N$, лежат внутри $N$-го отрезка — а ширина его, по архимедову свойству, делается меньше всякой наперёд заданной меры. Значит, любые два приближения, взятые после шага $N$, отстоят друг от друга не больше чем на ширину этого отрезка — то есть меньше всякой наперёд заданной $\epsilon$. А это и есть свойство Коши. ToS доказывает эту связь теоремой: процесс сжимающихся интервалов, задающий $\sqrt{2}$, есть процесс Коши.¹⁷

{ Здесь нужна точность, чтобы не сказать больше доказанного. Теорема shrinking_interval_Cauchy говорит о процессе особого рода — о процессе сжимающихся интервалов, удерживающем приближения во вложенных отрезках убывающей вдвое ширины. Ньютонов процесс и процесс цепной дроби из § 4.4 и § 4.5 — процессы иного типа: они порождаются своими формулами (усреднением, рекуррентой числителей и знаменателей), а не делением интервала пополам. Поэтому теорема о сжимающихся интервалах не доказывает автоматически, что ньютонов процесс или процесс цепной дроби суть процессы Коши: для каждого из них свойство Коши требует своей оценки погрешности. Точная картина такова: общий механизм сжимающихся интервалов показывает, что для того, чтобы процесс был числом-процессом, достаточно иметь рациональные стадии, удерживаемые во вложенных интервалах с шириной, уходящей к нулю; и процесс сжимающихся интервалов, задающий $\sqrt{2}$, этим механизмом и есть процесс Коши. Для ньютонова же и цепно-дробного процессов утверждение <<это процесс Коши>> нуждается в собственных оценках сходимости — и эти оценки в текущем виде RefinementSqrt.v не доказаны (§ 4.5).¹⁸}

Где проходит граница Части III

Здесь Часть III доходит до своего предела — и стоит сказать точно, где этот предел проходит.

Часть III установила: $\sqrt{2}$ даётся процессом — функциональной системой рациональных приближений (§ 4.4); процессов таких открытый класс (§ 4.5); всякий такой процесс достигает любой точности (§ 4.6) и есть процесс Коши (§ 4.7). Дальше этого Часть III не идёт — и не по недостатку, а по устройству замысла. Ибо за разобранным встают вопросы уже иного порядка. Процесс как самостоятельный предмет — не как процесс, дающий именно $\sqrt{2}$, а как объект сам по себе, со своим строением и своими отношениями, — требует отдельного построения. И вопрос, поставленный ещё в Главе III.3 (§ 3.7), — перечислимы ли процессы так же, как перечислимы рациональные числа, — остаётся не решённым: глава о счётности показала, что процесс есть поведение, а не данные, и оснований для перечислимости здесь нет, но доказать, что процессы не перечислимы, Часть III не берётся.

Эти вопросы составляют предмет Части IV. Часть III довела число-позицию до полноты и показала, что за нею разворачивается число-процесс; она разобрала первый такой процесс, $\sqrt{2}$, и установила о нём главное. Но процесс как таковой, действительные числа как процессы и несчётность процессов — всё это Часть IV строит заново и отдельно. Настоящая глава доводит изложение до порога; переступить его предстоит уже следующей части.

Сходимость процесса есть его внутреннее свойство: приближения, начиная с некоторого шага, неограниченно сближаются между собой. Это — свойство Коши, определяемое операционально, как поведение процесса. Процесс сжимающихся интервалов, задающий $\sqrt{2}$, обладает им доказанно: вложенные отрезки убывающей вдвое ширины удерживают приближения, а архимедово свойство ручается, что взаимное расстояние делается меньше всякой меры. Для процессов иного типа — ньютонова и цепно-дробного — свойство Коши требует собственных оценок сходимости. На этом Часть III доходит до своего предела: процесс как самостоятельный предмет и несчётность процессов — предмет Части IV.

Итог Части III. Переход к Части IV

Что прошла глава

Глава прошла путь от числа-позиции к числу-процессу.

Начала она с конкретной задачи: квадрат, равный двум, — длина диагонали единичного квадрата (§ 4.1). И показала, строгим доказательством бесконечного спуска, что ни одна позиция соразмерной разметки этой задаче не отвечает (§ 4.2). Глава развела уровни — уровень элемента и уровень системы — и показала, что условие $r\cdot r=2$ не посильно элементу-позиции, а посильно системе из элементов (§ 4.3). Такую систему глава и разобрала: $\sqrt{2}$ есть процесс — функциональная система, разложенная на правила, роли и элементы (§ 4.4). Процессов таких оказался открытый класс (§ 4.5); глава показала, что процесс достигает любой точности — по архимедову свойству (§ 4.6), — и что он есть процесс Коши: его приближения неограниченно сближаются между собой (§ 4.7).

Итог главы: $\sqrt{2}$ есть имя класса процессов — открытого семейства сходящихся функциональных систем, дающих квадрат, равный двум. Это — число-процесс: число, существующее позитивно на уровне систем, составленных из рациональных позиций.

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

{ Главный переход главы — от числа-позиции к числу-процессу — стоит закрепить разбором E/R/R (Часть I). По трём слоям систему $\sqrt{2}$ глава уже разложила в § 4.4, в онтологическом порядке, начиная с правил-конституции; сведём теперь разбор в таблицу — вобрав в неё и добавленное в § 4.5–4.7, — и проверим сформированность системы. Оговорка о статусе прежняя: <<система>> здесь — содержательная интерпретация по образцу функциональной системы Части I, не построенный в коде объект System $L$; единство процессов взято через слабое отношение process_equiv, а предикат sqrt2_process — формализация-цель (§ 4.4–4.5).}

Компонент	Что фиксирует	E/R/R
правило порождения и правило сходимости	конституция системы	Rule
единство процессов: process_equiv (слабое)	критерий тождества	Rule
архимедова достижимость; процесс Коши	условия сходимости	Rule
качество sqrt2_quality $=	x \cdot x - 2	$
рациональные приближения $1,3/2,17/12,\dots$	носители (конечны, $P4$)	Element
законы $L1$–$L5$ (здесь $L3$ для предела)	универсальный слой	Rule (универс.)

Хорошая сформированность. Разметка однозначна: два правила — конституция, качество приближения — роль, рациональные приближения — элементы; ни один слой не подменяет другого. Соблюдён и принцип $P1$ (нет самочленства): система $\sqrt{2}$ составлена из элементов уровнем ниже — наличных рациональных позиций, — а не из самой себя; уровень элемента и уровень системы глава развела ещё в § 4.3. И здесь разбор оборачивается диагностикой. Классическая картина <<$\sqrt{2}$ — недостающее число, прореха среди рациональных>> возникает от смешения категорий: роль, посильную лишь системе (<<давать в квадрате двойку>>), ищут среди элементов-позиций — и, не найдя, объявляют нехваткой. В верной разметке нехватки нет: роль несёт система из рациональных элементов, и $\sqrt{2}$ существует позитивно (§ 4.4). Честные границы при этом сохранены: sqrt2_not_in_Q доказано конструктивно (без $L3$), тогда как теория сжимающихся интервалов § 4.7 опирается на $L3$, — это разные статусы, смешивать их не следует.

Что даёт разбор. Он закрепляет весь путь Части III одним различением уровней. Целое, рациональное — это числа-позиции, роли, посильные элементу; $\sqrt{2}$ — первое число, чья роль посильна не элементу, а системе: число-процесс. E/R/R показывает, почему порог именно здесь — меняется не материал (элементы по-прежнему рациональны), а уровень носителя роли. Этим Часть III исчерпывает число-позицию и передаёт число-процесс Части IV, где процесс будет взят как самостоятельный предмет — со своим равенством, порядком и строением.

Что прошла Часть III

Настоящая глава завершает Часть III, и стоит окинуть взглядом весь её путь.

Часть III начала с натурального ряда, полученного в Части II, и спросила, что разворачивается из него дальше. Ответом стала череда координатных разметок. Глава III.1 развернула целые числа — двустороннюю координатную разметку с опорой и единичным шагом: знак минуса был прочитан не как отрицательное существование, а как противоположная ориентация смещения относительно опоры, и обе стороны разметки оказались равно продлеваемыми. Глава III.2 развернула рациональные числа — соразмерную разметку с дробным шагом, плотную, наследующую от целых чисел координатный смысл знака. Глава III.3 показала, что рациональные числа перечислимы, — построив явный конструктивный обход. И настоящая глава показала, что за рациональными числами разворачивается число-процесс, разобрав первый его образец — $\sqrt{2}$.

Весь этот путь — от натурального ряда до рациональных чисел — был путём числа-позиции. Натуральное число, целое, рациональное — все суть позиции координатной разметки, точки, взятые относительно опоры. Часть III довела эту мысль до полноты: построила разметки, показала их устройство, их асимметрию, их перечислимость — и дошла до порога, на котором число-позиция исчерпывает себя и за которым разворачивается число-процесс.

Позитивный итог

Стоит сказать, в каком модусе Часть III прошла этот путь, ибо модус был выдержан от первой главы до последней.

Часть III нигде не говорила о нехватке. Целые числа не <<восполняли ущерб>> натуральных; рациональные не <<латали прорехи>> целых; $\sqrt{2}$ не <<возмещало недостачу>> рациональных. Всякий раз разворачивалось новое — и разворачивалось из того, что уже было, прослеживанием того, что в нём заложено. Целые числа получились, когда акт различения был взят в обе стороны от опоры; рациональные — когда он был взят внутрь шага; число-процесс — когда обнаружилась роль, посильная не элементу, а системе. Ни одна числовая система не была ущербной; каждая была полна на своём уровне и каждая подводила к уровню следующему.

И $\sqrt{2}$ — последнее, к чему Часть III пришла, — есть итог именно позитивный. Не пустое место среди рациональных чисел, а богато устроенная функциональная система: открытый класс сходящихся процессов, каждый со своими правилами, ролями, элементами. Там, где привычный взгляд видел недостачу, ToS обнаружила избыток.

Переход к Части IV

Часть III довела изложение до порога, за которым лежит предмет Части IV.

Число-процесс глава разобрала на одном образце — на $\sqrt{2}$. Но $\sqrt{2}$ — лишь первый из процессов, и процесс был взят здесь как процесс, дающий именно его. Часть IV возьмёт процесс как таковой — как самостоятельный предмет, со своим строением, своими отношениями, своим равенством и порядком. Она построит действительные числа — не как позиции, а как процессы. И она вернётся к вопросу, оставленному открытым ещё Главой III.3 и подтверждённому настоящей главой: перечислимы ли процессы? Здесь Часть IV должна будет уточнить, о каком классе процессов идёт речь. Вычислимые процессы, заданные конечными правилами или программами, перечислимы именно как программы — как конечные выражения над счётным алфавитом (Глава III.3). Но произвольные процессы-поведения, функции $N\to Q$, к совокупности конечных программ не сводятся, и соответствующее пространство процессных поведений имеет иной статус. Часть III показала, что процесс есть поведение, а не данные, и что для перечислимости произвольных процессов оснований нет; Часть IV докажет несчётность — и докажет её не для <<процессов вообще>> в смысле программ, а для пространства процессных поведений, аккуратно очертив, какой именно класс процессов имеется в виду.

На этом Часть III завершается. Она прошла путь числа-позиции от натурального ряда до рациональных чисел, довела его до полноты и дошла до порога, за которым разворачивается число-процесс. Переступить этот порог и построить действительные числа как процессы предстоит Части IV.

---

---

Часть: Часть III. От натуральных к рациональным · Том: «Математика»

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

Навигация: ← Глава 3. Счётность рациональных чисел · Глава 1. P4: бесконечность как процесс — Часть IV →

Footnotes

1. Доказательство, излагаемое в этом разделе, формализовано в файле Sqrt2Irrational.v Rocq-репозитория ToS (каталог analysis). Файл содержит 14 доказанных утверждений, не опирается ни на одну аксиому и не пользуется законом исключённого третьего. ↩

2. Лемма sq_even_implies_even файла Sqrt2Irrational.v: если $n\cdot n$ чётно, то $n$ чётно. ↩

3. Это — лемма sq_eq_2sq_both_even файла Sqrt2Irrational.v. ↩

4. Шаг спуска — лемма descent_step файла Sqrt2Irrational.v: из $p^2=2q^2$ строятся $p^{\prime }=p/2$ и $q^{\prime }=q/2$ с тем же $p^{\prime 2}=2q^{\prime 2}$. ↩

5. Это — лемма descent_to_zero файла Sqrt2Irrational.v, доказанная сильной индукцией (Rocq: lt_wf_ind) по мере $|p|+|q|$, точнее по $‘Z.t{o}_{n}at‘(|p|+|q|)$: всякое решение $p^2=2q^2$ есть $p=0$, $q=0$. Каждый шаг спуска строго уменьшает эту меру, а бесконечно убывающей цепи натуральных мер быть не может. ↩

6. sqrt2_not_in_Q файла Sqrt2Irrational.v: $\neg (\exists r:Q,r\cdot r==2)$. Предикат <<квадрат равен двум>> не реализуется ни одним элементом типа $Q$. ↩

7. Процессы, разбираемые в этом разделе и в следующем, формализованы в файле RefinementSqrt.v Rocq-репозитория ToS (каталог stdlib). Файл определяет процессы sqrt2_newton и sqrt2_cf и доказывает их конкретные значения на первых шагах; о границах доказанного см. § 4.5. ↩

8. В файле RefinementSqrt.v качество приближения определено функцией sqrt2_quality, сопоставляющей числу $x$ величину $|x\cdot x-2|$. ↩

9. Оба процесса — ньютонов и цепной дроби — и сравнение их формализованы в файле RefinementSqrt.v Rocq-репозитория ToS. ↩

10. Совпадение на шагах $0$ и $1$ доказано в RefinementSqrt.v леммами agree_at_0 и agree_at_1. ↩

11. Что приближения двух процессов на шаге $2$ различны, доказано леммой differ_at_2 файла RefinementSqrt.v. ↩

12. Что на шаге $2$ ньютоново приближение точнее — меньше по величине качества sqrt2_quality — доказано леммой newton_better_at_2; совпадение на ранних шагах и расхождение с преимуществом Ньютона на шаге $2$ сведены в теорему sqrt2_strict_refinement файла RefinementSqrt.v. ↩

13. process_equiv (нотация \~{}\~{}) файла ProcessCore.v; там же доказаны process_equiv_refl, process_equiv_sym, process_equiv_trans. Отметим для точности, что в текущем виде глава использует process_equiv как готовое определение из репозитория, но теорема <<ньютонов процесс и процесс цепной дроби эквивалентны по process_equiv>> в репозитории ещё не доказана; глава указывает это отношение как то, которым единство процессов должно быть выражено. ↩

14. Архимедово свойство в этой форме — теорема Archimedean файла Archimedean_ERR.v Rocq-репозитория ToS: для всякого $\epsilon >0$ существует $N$, для которого $1/2^N<\epsilon$. Файл содержит 14 доказанных утверждений и не вводит ни одной аксиомы; в частности, не используется никакая аксиома бесконечности. ↩

15. Файл Archimedean_ERR.v прямо отмечает, что архимедово свойство есть утверждение о процессах: для всякой точности процесс деления пополам её достигает, и завершённой бесконечности для этого не требуется. ↩

16. Определение is_Cauchy и теоремы этого раздела — в файле ShrinkingIntervals_ERR.v Rocq-репозитория ToS. Стоит оговорить: в разных файлах формализации используются эквивалентные технические варианты условия Коши — с индексами $n>N$ (как в ShrinkingIntervals_ERR.v и Archimedean_ERR.v) либо с индексами $N\le n$ (как в файле ProcessCore.v). Содержательно они выражают одно и то же — начиная с некоторого шага, все дальнейшие члены процесса взаимно близки, — и переводятся друг в друга сдвигом индекса на единицу; глава поэтому не говорит о едином определении, а о содержательно одном свойстве в эквивалентных записях. ↩

17. Теорема shrinking_interval_Cauchy файла ShrinkingIntervals_ERR.v: если ширина вложенных интервалов убывает как половинные доли, то процесс, держащийся внутри них, удовлетворяет свойству is_Cauchy. Доказательство опирается на архимедово свойство (§ 4.6). ↩

18. Стоит отметить и различие в логическом окружении файлов. Доказательство иррациональности $\sqrt{2}$ (§ 4.2, файл Sqrt2Irrational.v) полностью конструктивно — без закона исключённого третьего. Общий же файл ShrinkingIntervals_ERR.v работает в классическом окружении ToS: он импортирует ToS_Axioms и классическую логику (Classical_Pred_Type) для некоторых предельных аргументов, и комментарий файла это прямо оговаривает. Это не новая аксиома настоящей главы, а использование уже принятого формального слоя ToS — закона исключённого третьего $L3$, входящего в основания (Часть I). Конструктивность доказательства $\sqrt{2}\notin Q$ и опора на классическую логику в общей теории сжимающихся интервалов — разные статусы, и смешивать их не следует. ↩