57. Канон вполне-фундированности: молоток доходит до классики завершаемости¶
← 56. Первопричина Коллатца · Оглавление
Двигатель — один запрет: нет бесконечной строго убывающей цепи на вполне-фундированном носителе
(no_perpetual_engine_of_wellFounded), и он переносится по любому рангу в вполне-фундированный
порядок (no_perpetual_engine_of_rank, 01). Каждый фронт до сих пор был следствием этой
единственной теоремы. Теперь направим её туда, где ей всего родней, — на классический канон
завершаемости, результаты, чьё всё содержание есть бесконечного спуска нет. Каждый становится
зелёным инстансом, реюзая уже готовое в mathlib; ни один не добавляет аксиомы, и таинт не двигается.
Гидра умирает¶
Гидра Кирби–Пэриса: отрубаешь голову — вырастает конечное число новых, ниже; всегда ли кончается битва? Здесь ответ — двухстрочное следствие.
Теорема 57.1 (hydra_no_perpetual_engine, 🟢). Битва гидры не несёт вечного двигателя: для любого
вполне-фундированного r отношение среза Relation.CutExpand r не допускает бесконечной убывающей
последовательности.
Почему это верно. Срез гидры — ровно один шаг Relation.CutExpand (убрать голову a, добавить
конечно много a' с r a' a). Mathlib доказывает WellFounded r → WellFounded (CutExpand r)
(WellFounded.cutExpand); подаём это в no_perpetual_engine_of_wellFounded. Гидра умирает, потому что
её состояние спускается по вполне-фундированному порядку — двигатель, дословно.
ω-червь: трансфинитный ранг¶
До сих пор всякий ранг был натуральным числом. Но двигатель переносится по рангу в любой вполне-фундированный порядок, а ординалы — архетип. Вот первый трансфинитный инстанс, и он схватывает самый глубокий трюк канона.
Теорема 57.2 (omega_worm_no_perpetual_engine, 🟢). Читаем состояние как (a, b) — большой
регистр a, малый регистр b. Шаг роняет a на единицу и позволяет b прыгнуть на ЛЮБОЕ значение.
Процесс всё равно завершается — не несёт вечного двигателя — под ОРДИНАЛЬНЫМ рангом ω·a + b.
Почему это верно. Хотя b может взрываться как угодно, ординал строго роняется: ω·a + k <
ω·(a+1) + b' при любом k, ибо k < ω. Значит no_perpetual_engine_of_rank с областью значений
Ordinal (а не ℕ) закрывает это — первый трансфинитный ранг в программе. Это ровно механизм за
теоремой Гудстейна и гидрой: натуральное значение растёт неограниченно, а ординальный ранг падает,
и падающие ординалы не могут падать вечно. Полный слабый Гудстейн — цифры по основанию b, прочитанные
как ординал ниже ω^ω, — естественное продолжение того же ранга, и мы отмечаем его как следующий шаг
(здесь ещё не формализован).
Спуск Маркова: зелёная стена и красные ворота¶
Теорема 57.3 (markov_no_perpetual_engine, 🟢). Дерево Маркова троек x²+y²+z²=3xyz сводится к
корню: бесконечной цепи прыжков Виеты z ↦ 3xy−z нет, ибо высота x+y+z — строго убывающий ℕ-ранг
(markov_vieta_lt).
Почему это верно. Из упорядоченной некорневой тройки x ≤ y ≤ z при y < z прыжок Виеты заменяет
z на z' = 3xy − z, и z' ≤ y < z — ибо y лежит между двумя корнями t² − 3xy·t + (x²+y²), так
что верх строго падает, а с ним и высота. Замкнутость Виеты (isMarkov_vieta) держит новую тройку
марковской; высота, будучи натуральным числом, не может спускаться вечно.
Это маска: половина завершаемости/конечности зелена, но она ничего не говорит о гипотезе единственности Фробениуса — что всякое число Маркова есть наибольшая координата единственной тройки, открыта с 1913. Единственность — инъективность метки-максимума, ортогональна фундированности; молотку там не за что зацепиться. Зелёная стена, честные красные ворота — та же форма, что у проблем тысячелетия.
Разделяющая линия обратимости¶
У двигателя есть обратная сторона, и канон её называет. Там, где строгий спуск не возвращается, обратимая система возвращается всегда.
Теорема 57.4 (poincare_dividing_line, 🟢). Две половины на пространстве с мерой. (i) Всякое
вполне-фундированное отношение запрещает вечный двигатель — убывающую цепь, а значит и всякий возврат.
(ii) Консервативное отображение (например, сохраняющее конечную меру, обратимое) удовлетворяет возврату
Пуанкаре: почти всякая точка множества возвращается в него бесконечно часто.
Почему это верно. Первая половина — двигатель (no_perpetual_engine_of_wellFounded); вторая —
mathlib-евский Conservative.ae_mem_imp_frequently_image_mem. Вместе они — те самые противоположности,
что universal_engine_dividing_line называет на ℝ, теперь на динамической системе: строгий спуск на
вполне-фундированном носителе не возвращается никогда; сохраняющая меру обратимость — всегда. Это
замыкает ось обратимости, вскрытую квантовым прочтением (гл. 50): замкнутая, унитарная,
обратимая эволюция возвращается; наш необратимый спуск — не может.
Континуум реализует двигатель — и именно поэтому на него нельзя нажать¶
Последнее заострение замыкает круг с universal_engine_dividing_line: двигатель реализован на ℝ
(perpetualEngine_on_real, спуск (1/2)ⁿ → 0) и запрещён на вполне-фундированной ℕ
(no_perpetual_engine_on_nat). Соблазн — инвертировать арифметическую лестницу в (0,1) и бесконечным
дроблением континуума выбить арифметическую бесконечность даром. Так нельзя, и вот ровно почему.
Теорема 57.5 (strictAnti_meets_nat_finitely, 🟢). Строго убывающая, ограниченная снизу
вещественная последовательность принимает натуральные значения лишь конечно часто.
Почему это верно. Её целые значения были бы бесконечным строго убывающим множеством натуральных в
ограниченном интервале — невозможно (фундированность ℕ). Значит ℝ-двигатель спускается вечно сквозь
зазоры — свидетель (1/2)ⁿ целый лишь при n = 0 — и структурно слеп к ℕ-скелету. Это
no_perpetual_engine_on_nat в аналитической одежде: причина, по которой реализованный ℝ-двигатель не
несёт арифметики.
Теорема 57.6 (twinCenters_accumulate_at_zero_iff_infinite, 🟢). Ноль — предельная точка
инвертированных twin-центров {1/m} (по twin-центрам m) тогда и только тогда, когда twin-центров
бесконечно много.
Почему это верно. Бесконечно много центров дают сколь угодно большие m, и 1/m входит в любую
окрестность 0; конечно много дают конечное замкнутое множество без точек накопления. Обе стороны
доказаны без теории чисел — над непрозрачным предикатом — так что теорема аксиомо-чиста и, главное,
не вносит доказательства. Инверсия m ↦ 1/m — биусловное переодевание: «близнецы жмутся к
первопричине 0» есть то же самое утверждение, что гипотеза близнецов, в одежде ℝ-топологии, ровно с
тем же содержанием и не более.
Так наблюдатель на большом twin-центре, глядя вниз по инвертированной лестнице к 0 — могиле нуля,
первопричине, — видит скучивание близнецов у истока тогда и только тогда, когда их бесконечно; а
сертифицировать это скучивание значило бы завершить бесконечный спуск ℕ-скелета, запрещённый двигатель.
Континуум даёт двигатель даром именно потому, что не несёт целых точек. Брун заостряет против
соблазна: обратные близнецам сходятся (константа Бруна), так что их скучивание у 0 — самый тонкий,
самый континуум-невидимый сигнал из всех; а сходимость безразлична к мощности; единственный реципрокальный
феномен, что принуждает бесконечность, — расходимость ∑1/p = ∞ — ровно тот, что близнецы не дают. Это
усиление наблюдения, а не шаг к гипотезе.
Примечание (что доказано, что отложено, что не подходит).
- ω-червь (57.2) — трансфинитно-ранговый механизм Гудстейна и гидры, а не полная теорема слабого Гудстейна; цифровой ординал по основанию
b— естественный следующий шаг, отложен.- Отложенное зелёное: полный слабый Гудстейн (через
Nat.digitsи ординальную нормальную форму Кантора), лемма Ньюмана (завершаемость ⇒ конфлюэнтность, в mathlib как абстрактный результат отсутствует), инстансы вполне-квази-порядка Хигмана/Диксона.- Задокументированные не-совпадения — молоток до них явно не доходит: аликвотные последовательности (Каталан–Диксон) — нет вполне-фундированного порядка, а ограниченность скорее ложна; Эрдёш–Штраус
4/n = 1/a+1/b+1/c— препятствие покрытия, не спуск; пятнашки и паритетные игры — сохраняющийся инвариант, ортогональный убывающему рангу; устойчивость материи, КАМ, упаковки сфер — настоящий анализ без дискретного вполне-фундированного носителя в Lean.- Размещение относительно Гёделя заострено в Коде (50): именно здесь «не гёделев феномен» надо читать точно — фундированность, а не самоссылка.
Место в общем ходе¶
Семь масок читают трудные аналитические объекты как тени запрета; здесь запрет встречает объекты, которые и есть запрет, названный прямо. Гидра, червь, дерево Маркова — теоремы завершаемости, а завершаемость есть фундированность, а фундированность есть двигатель. Единственная новая математика — это оправа; и один трансфинитный ранг, который показывает, что двигатель никогда не был привязан к числовой прямой: он работает всюду, где спуск можно измерить ординалом, что не падает вечно.