Глава 6. P4 как фильтр

Зачем главе фильтр

Пять переустановок и шаг назад

Часть IV прошла пять переустановок. Бесконечность стала процессом, а не готовым множеством (Глава 4.1). Действительное число стало процессом рациональных приближений, а не точкой-атомом (Глава 4.2). Точка стала классом эквивалентных процессов, а не первичной данностью (Глава 4.3). Несчётность стала невозможностью регулярного перечисления охватить все классы, а не свойством завершённого множества (Глава 4.4). Континуум стал структурной дихотомией замкнутых совокупностей, а не несчётным множеством или мерой мощности (Глава 4.5).

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

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

Итог Части IV

Прежде чем назвать дисциплину, окинем взглядом весь ход Части IV — ибо именно его материал глава и будет классифицировать.

Часть начиналась с тревоги: если принять $P4$ — если бесконечность есть лишь свойство процесса, а завершённых бесконечных объектов нет, — не рухнет ли вместе с ними классический анализ действительного числа? Пять глав отвечали на эту тревогу, и ответ сложился такой. $P4$ не уничтожает основные структуры анализа; она меняет их носитель. Бесконечность перестаёт быть готовым множеством и становится процессом, незавершаемым, но в каждый момент конечным (Глава 4.1). Действительное число перестаёт быть точкой и становится процессом рациональных приближений (Глава 4.2). Точка перестаёт быть первичной и становится классом эквивалентных процессов (Глава 4.3). Несчётность перестаёт быть свойством завершённого множества и становится невозможностью процессного перечисления охватить все классы (Глава 4.4). Континуум перестаёт быть несчётным множеством и становится структурной дихотомией (Глава 4.5).

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

$P4${P4} как фильтр: центральный тезис

Дисциплину же, о которой идёт речь, можно назвать одной формулой. До сих пор $P4$ выступала как онтологический принцип: бесконечность есть свойство процесса. Но у неё есть и вторая, методологическая роль.

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

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

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

Глава устроена так. Сперва — две шкалы силы, в которых ToS оценивает свои результаты: шкала силы деривации (§ 6.2) и шкала IF-условий (§ 6.3). Затем — разбор самого фильтра как системы E/R/R (§ 6.4). Затем — применение фильтра к математическому корпусу Тома II (§ 6.5): что в нём доказано, что принято, что выбрано. Затем — две стороны фильтра: что $P4$ отсекает (§ 6.6) и что оставляет (§ 6.7). Затем — честный каталог открытого (§ 6.8). И наконец — итог Части IV и место Тома II в ландшафте оснований (§ 6.9).

Сила деривации: пять градаций

Зачем шкала

Сказать о результате «он доказан» недостаточно — нужно сказать, в какой мере он связан с исходными началами. Одно дело — утверждение, вытекающее из $P1$–$P4$ чистой алгеброй, без единого выбора. Другое — утверждение, верное при некотором дополнительном допущении. Третье — утверждение, лишь совместимое с началами, но ими не вынужденное. Эти случаи нельзя смешивать, и ToS их различает формальной шкалой.

Пять градаций

Шкала введена в Rocq-репозитории типом DerivationStrength с пятью значениями.¹ Вот они, от сильнейшей к слабейшей:

Градация	Что означает
FullyDerived	следует из $P1$–$P4$ одних, без выборов
DerivedWithInput	выведено при заданном параметре-входе
Constrained	начала сужают до конечного числа возможностей
ConsistentWith	совместимо с началами, но ими не вынуждено
ExternalInput	постулировано, не выведено

Здесь нужна точность о материале шкалы. В самом файле эта шкала применена прежде всего к результатам будущего физического слоя — не к математике настоящего тома. Файл классифицирует физические результаты: одни помечены FullyDerived (их в его счёте три), другие DerivedWithInput (два), Constrained (два), ConsistentWith (один); итог — восемь классифицированных результатов (теорема total_classified). Сами эти результаты — предмет другого тома; здесь существенна не их природа, а сама шкала, которую мы возьмём как инструмент.

Документированный мета-аудит, а не сканер

О статусе этого файла надо сказать прямо, чтобы не возникло ложного впечатления. ProcessAxiomAudit.v не есть автоматический обходчик зависимостей, который сам сканирует репозиторий и размечает каждую теорему. Это документированный мета-аудит: разметка силы внесена автором на основании результатов команды Print Assumptions, запускаемой отдельно для каждой теоремы. Файл фиксирует вывод этого аудита как набор определений и проверяемых лемм (например, fully_derived_strongest), но сам по себе ничего не сканирует.

Ту же оговорку файл несёт и о аксиомной цене. Его теорема axiom_minimal утверждает содержательно: ключевые результаты зависят только от classic — то есть от $L3$, закона исключённого третьего, — а закон достаточного основания L4_witness локализован и появляется лишь в отдельных файлах (лемма l4_witness_localized). Аксиомы выбора, бесконечности, унивалентности, функциональной экстенсиональности не используются. Это документированное утверждение об аудите, опертое на Print Assumptions, а не машинная проверка всего репозитория одной командой.

IF-условия: Forced / Natural / Chosen

Вторая шкала

Шкала силы деривации отвечает на вопрос «насколько результат связан с началами». Вторая шкала уточняет первую с иной стороны: она спрашивает, какого рода условие стоит перед результатом. Эта шкала — тип IFStrength — введена в отдельном файле² и имеет три значения: Forced (следует из $P1$–$P4$ без выбора), Natural (простейший, родовой случай, но не вынужденный) и Chosen (определённый выбор среди нескольких возможностей).

Следует против совместимо

Различие, которое обе шкалы вместе проводят, есть фундаментальное различие зрелой теории: между «$X$ следует из начал» и «$X$ совместимо с началами». Первое означает: отвергнуть $X$, приняв начала, нельзя. Второе означает лишь: $X$ можно принять, не впадая в противоречие с началами, — но можно и не принять. Теория, не различающая этих двух, выдаёт совместимость за выводимость и тем завышает свою силу.

И здесь файл честен в счёте. Из двенадцати разобранных в нём выводов Forced оказались четыре, Natural — пять, Chosen — три (леммы derivation_count_forced, derivation_count_natural, derivation_count_chosen). Не всё выведено — и это сказано прямо, числом.

<<Не всё выведено>> как честность

Признание, что лишь треть выводов Forced, а прочие Natural или Chosen, — не слабость теории, а её зрелость. Теория, у которой всё Forced, либо тривиальна, либо нечестна: она либо ничего содержательного не утверждает, либо выдаёт свои выборы за необходимости. Сила теории не в том, чтобы всё объявить вынужденным, а в том, чтобы точно знать и прямо называть, что вынуждено, что естественно и что выбрано. Две шкалы ToS и служат этому знанию.

Разбор E/R/R: фильтр деривации как система

Фильтр по трём слоям

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

Rules. Конституция системы-фильтра — два правила классификации: шкала силы деривации (DerivationStrength, § 6.2) и шкала IF-условий (IFStrength, § 6.3). К ним — правило честного учёта: статус каждого результата определяется не желанием, а аудитом его зависимостей (Print Assumptions, документированный).

Roles. Роли — сами статусы силы: FullyDerived, DerivedWithInput, Constrained, ConsistentWith, ExternalInput по одной шкале; Forced, Natural, Chosen — по другой. Каждый результат занимает место в этой сетке статусов, и место это есть его роль в системе знания: не «что доказано», а «с какой силой связано с началами».

Elements. Элементы — сами результаты тома (теоремы, построения, интерпретации), которые фильтр и распределяет по статусам. По $L1$ каждый результат тождествен себе; по $P4$ их конечный, наличный список — то, что уже построено, — и есть материал классификации.

Сформированность и диагностика

Хорошая сформированность. Разметка однозначна: результаты — элементы, статусы силы — роли, две шкалы — правила. Соблюдён принцип $P1$ (нет самочленства): фильтр классифицирует результаты, а не себя; шкала не есть один из своих результатов. И здесь разбор оборачивается диагностикой — той, ради которой фильтр и нужен. Смешать роль ConsistentWith с ролью FullyDerived — прочитать <<совместимо>> как <<выведено>> — есть смешение категорий: элементу приписывают чужую, более высокую роль. Это в точности то завышение, которое фильтр ловит. Зрелость теории измеряется не числом FullyDerived-результатов, а точностью разметки.

Фильтр на математике Тома II

Авторская ретроспектива, не Coq-таблица

{ В самих мета-файлах шкалы применены прежде всего к результатам будущего физического слоя. В этой главе мы используем те же шкалы как ретроспективный инструмент для математического корпуса Тома II. Это авторская классификация по уже доказанным результатам, а не отдельная Coq-таблица, автоматически размечающая Главы II–IV. В репозитории нет файла, который перечислял бы математические теоремы тома с их статусами силы; разметка ниже выведена автором из самих глав и из их аксиомной цены, проверяемой командой Print Assumptions.}

Две независимые оси

Разметку стоит вести по двум осям, ибо они связаны, но не совпадают. Первая ось — аксиомная цена: сколько и каких логических аксиом стоит за результатом (ноль; один $L3$; два $L3$ и $L4$). Вторая ось — тип силы вывода: вынужден ли результат началами или есть выбор представления. Низкая аксиомная цена не то же, что полная выводимость: результат может быть конструктивным (ноль аксиом) и при этом опираться на выбор модели; и наоборот. Нулевая аксиомная цена говорит о чистоте доказательства внутри выбранной формализации; FullyDerived говорит о силе связи результата с началами. Это разные суждения.

Срез математических результатов

Применим обе оси к ключевым результатам Частей II–IV.

Статус	Математические результаты тома
0 аксиом, конструктивно	счётность $Q^{+}$ через дерево Калкина–Уилфа (Глава III.3, Countability_Q.v); иррациональность $\sqrt{2}$ конструктивно, без $L3$ (Глава III.4, Sqrt2Irrational.v); базовые процессные конструкции RealProcess/is_Cauchy/ process_equiv (ProcessCore.v)
$L3$ (classic)	несчётность процессов единичного интервала относительно регулярных перечислений (Глава 4.4)
$L3+L4$	дихотомия Кантора–Бендиксона для замкнутых совокупностей бинарных процессов (Глава 4.5; $L4$ — в счётном объединении)
Выбор модели или представления	бинарная модель $2^N$ против модели Коши (Глава 4.5); выбор представителя класса, регистрация единицы (Глава II.1), формат кодирования

Срез этот честен в обе стороны. С одной стороны, ядро тома стоит дёшево и твёрдо: счётность рациональных и иррациональность $\sqrt{2}$ не стоят ни одной аксиомы и доказаны конструктивно; процессная арифметика — тоже. С другой стороны, два центральных результата Части IV опираются на логические аксиомы — несчётность на $L3$, дихотомия на $L3$ и $L4$, — и это надо называть, не пряча. И наконец, ряд развилок есть выбор, а не вывод: какая модель континуума, какой представитель класса, с какого числа считать, — здесь ToS выбирает осознанно, и выбор этот — роль Chosen, не Forced.

Что $P4${P4} отсекает

Завершённую бесконечность как первичный носитель

Главное, что $P4$ отсекает, — это завершённая бесконечность как исходный онтологический носитель. Не аксиому бесконечности как запись в языке Rocq (тип nat и функциональные типы — законные типы языка, § 4.1), а постулат о готовом бесконечном множестве как актуальном, разом данном объекте. Где классика берёт завершённую числовую прямую, завершённое множество всех натуральных, несчётное множество точек — там $P4$ не признаёт исходного объекта и требует процесс. Это отсечение Часть IV провела ретроспективно на пяти образцах (§ 6.1): всякий раз завершённый объект заменялся процессным носителем.

Импредикативные completed-set конструкции — как носители

Осторожнее надо с импредикативностью. Было бы неверно сказать, что $P4$ <<отсекает импредикативность вообще>>: логический уровень Prop\ в Rocq сам несёт импредикативные черты, и многие файлы тома работают на этом уровне (совершенное ядро § 4.5 — Prop-значный свидетель). $P4$ не запрещает Prop\ как логический уровень. Что $P4$ отсекает — это превращение импредикативно заданных совокупностей в первичные онтологические объекты анализа: определять действительное число или континуум через совокупность, квантифицирующую саму себя как готовый предмет. Логический инструмент Prop\ остаётся; запрещён лишь его онтологический перевод в завершённый объект-носитель.

Внешнюю аксиому выбора — но не закон свидетельствования

И отдельно — об аксиоме выбора, ибо здесь легче всего сказать слишком много. $P4$ не использует внешнюю теоретико-множественную Аксиому Выбора как онтологический принцип построения объектов: акта одновременного выбора по завершённому семейству множеств в процессной онтологии нет. Но было бы неточно сказать <<выбора нет вовсе>>. В ToS есть $L4$ — закон достаточного основания, в формализации L4_witness, — и он выполняет работу, похожую на выбор, но на уровне свидетелей: из доказательства существования он извлекает конкретный свидетель. В Главе 4.5 этот закон прямо работает — в счётном объединении перечислимых семейств (countable_union_enum) он извлекает для каждого класса его перечислитель. Поэтому корректная формула не <<выбора нет>>, а такая: нет внешней ZFC-аксиомы выбора; есть локальный закон свидетельствования $L4$ внутри ToS — choice-подобный по технической силе, но не теоретико-множественный по существу.

Что $P4${P4} оставляет

Ретроспективная таблица построенного

Отсечению отвечает сохранение. И здесь важно не повторять разговор Главы 4.1 о том, почему $P4$ то или иное допускает, а назвать прямо, что за пять глав построено или обосновано на процессных носителях. Сведём это в таблицу процессных форм, построенных или обоснованных в Главах 4.1–4.5.

Классический предмет	Что $P4$ оставляет (процессная форма)
бесконечность	процесс порождения, незавершаемый, в каждый момент конечный
действительное число	процесс Коши — RealProcess, сходящаяся последовательность рациональных приближений
точка	setoid-класс эквивалентных представителей (по process_equiv)
несчётность	невозможность регулярного обхода охватить все классы
континуум	дихотомия замкнутых бинарных совокупностей (перечислимое либо совершенное)

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

Что остаётся открытым

Рабочая карта, а не файл репозитория

{ Зрелость теории видна и в том, что она прямо называет несделанное. Ниже — рабочая нумерация backlog’а $F$-задач. Это не имена Coq-теорем и не файл репозитория: это карта открытых формализационных задач, выведенная из предыдущих глав тома и собранная автором. (В коде $P4$-программы есть свой каталог открытого — файл ProcessOpenQuestions.v, <<что осталось>>; но его пункты — физические, и сама его честная итоговая оценка дана для физического слоя. Здесь же речь о математических задачах настоящего тома.)}

Открытые задачи математики тома

Главные открытые задачи таковы.

Фактортип точек не построен ($F$-10). Точка держится на setoid- чтении — классе по process_equiv; настоящего фактортипа, где эквивалентные процессы суть один терм, в репозитории нет. На нём стоят и метрика, и топология на классах.

Полное перечисление $Q$ ($F$-17). Дерево Калкина–Уилфа перечисляет лишь положительные рациональные; полная биекция $N\leftrightarrow Q$ со знаком и нулём — стандартное расширение, теоремой не закреплённое.

Мост между моделями ($F$-19). Действительные как процессы Коши (Главы 4.2–4.4) и континуум как $2^N$ (Глава 4.5) живут в разных моделях; перевода между ними — $2^N\leftrightarrow [0,1]$ — в коде нет.

Деривация $L1\text{wedgeL}5\text{RightarrowP}4$ ($F$-18). Вывод самого принципа $P4$ из законов проведён в томе содержательно, а не машинно: в коде $P4$ стоит самостоятельным предикатом, без формальной цепочки от законов.

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

Итог Части IV и место Тома II

Куда фильтр идёт дальше

Фильтр, разобранный на математике тома, не кончается на ней. Самые содержательные его применения — впереди, в физическом слое, откуда взяты обе шкалы (§ 6.2–6.3). Именно там фильтр различает: что выведено из принципов, что совместимо с ними, что выбрано как параметр, а что лишь постулировано. Примеры тех файлов — величины и соотношения физики — предмет другого тома; здесь важно, что дисциплина фильтра уже выработана и проверена на математике, прежде чем быть применённой к более спорному материалу.

Место Тома II в ландшафте оснований

И последнее. Том II не есть ещё одна аксиоматика, соперничающая с теорией множеств за право быть основанием. Он есть переустановка носителя: та же математика — число, точка, предел, континуум, — но на процессе вместо завершённого множества, с явно размеченной аксиомной ценой — прежде всего $L3$ и локально $L4$ — вместо неявного сет-теоретического фона, с честной разметкой силы каждого результата. ToS не спорит со стандартной математикой о теоремах; она предлагает иное прочтение того, из чего математика сделана, — и фильтр $P4$ есть то, что удерживает это прочтение от завышения.

Итог главы — в трёх частях. Первое: что сделано. $P4$ прочитана не только как онтологический принцип процессов, но и как фильтр допустимой силы утверждения — различающий вынужденное, естественное, выбранное, совместимое и внешнее; этот фильтр применён ретроспективно к математике Тома II. Второе: на чём это стоит. Две шкалы — DerivationStrength и IFStrength — введены в коде на физическом материале; здесь они взяты как инструмент, а разметка математики тома — авторская, опертая на Print Assumptions, не отдельная Coq-таблица. Ядро тома стоит на нуле аксиом, два результата Части IV — на $L3$ и на $L3+L4$; внешней аксиомы выбора нет, но есть choice-подобный закон свидетельствования $L4$. Третье: что остаётся открытым. Фактортип точек, полное перечисление $Q$, мост между моделями, машинная деривация $P4$ из законов — рабочая карта, не доказанные теоремы. Этим Часть IV завершается: не сбережением всего анализа разом, а показом, как $P4$ перестраивает его на процессных носителях, — и честной разметкой силы каждого шага.

---

---

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

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

Навигация: ← Глава 5. Процессный континуум · Глава 1. Метрика на процессах — Часть V →

Footnotes

1. Тип DerivationStrength и его применения — в файле ProcessAxiomAudit.v Rocq-репозитория ToS (каталог src/process/). ↩

2. ProcessDerivedVsConsistent.v Rocq-репозитория ToS; тип IFStrength, запись DerivationRecord, список all_derivations. ↩

3. E/R/R-разметка в шапках ProcessAxiomAudit.v и ProcessDerivedVsConsistent.v. ↩