Cubic squeeze: короткий train¶
← 06. Нет хода назад · Оглавление · 08. Ограниченный цикл →
Lean:
EuclidsPath/Engine/Squeeze.lean(cubic_squeeze,cubic_squeeze_sq_lt).
Где мы¶
В предыдущей главе мы установили необратимость на двух точках: диагональ \(\sum_p X_p Y_p\) исчезает, один и тот же простой не сидит на обеих сторонах, и двигатель Евклида не работает назад (06 NoBackward). Необратимость запрещает возврат.
Но остаётся вопрос о дальности хода вперёд: когда двигатель, спускаясь, порождает повторяющийся атом и пытается разложить его вдоль одной аффинной линии индексов, — как далеко тянется этот «состав» (train) реально достижимых центров? В этой главе мы покажем, что, несмотря на бесконечность самой линии, её валидный сегмент короток: он зажат кубической связью между высотой атома и активным масштабом.
Постановка: атом, его повтор и линия индексов¶
Напомним координаты двигателя. Активный порог мы обозначаем \(A\): это масштаб, отделяющий «старые» малые простые \(p \le A\) от «новых» больших множителей \(>A\), участвующих в rank-разложении сторон \(6m \pm 1\) (04 Descent); напомним, ранг — это «высота» состояния, строго падающая вдоль разрешённых шагов (см. словарь). Когда descended-центр воспроизводит структурно то же евклидово уравнение меньшего масштаба, возникает повтор атома (repeated atom) — самоподобный шаг из каталога §23.
Введём высоту атома \(h \in \mathbb{N}\) — целочисленный параметр, измеряющий, насколько глубоко тянется повтор одного и того же множителя вдоль аффинной линии индексов \(n \mapsto N_0 + q\,n\). Линия эта бесконечна: формально индекс \(n\) пробегает все натуральные числа, и топливо \(+1\) (шаг индекса) никогда не иссякает. Именно поэтому наивно кажется, что состав повторов может быть сколь угодно длинным.
Наблюдение, которое мы формализуем, состоит в обратном. Стоимость повтора растёт не линейно, а кубически по \(h\), тогда как бюджет ограничен активным масштабом \(A\). Отсюда — жёсткий потолок на \(h\).
Примечание. Слово «train» здесь — не поезд-метафора ради образности, а точное имя объекта: последовательность реально достижимых центров вдоль одной аффинной линии. Бесконечность линии (носителя индексов) и конечность её валидного сегмента (train'а) — разные вещи, и всё содержание главы в том, чтобы их развести.
Определение стоимости повтора¶
Из каталога §23 стоимость повтора атома высоты \(h\) при активном масштабе \(A\) подчинена кубическому порогу
Раскрывая скобки и переходя к честной целочисленной форме (без извлечения корня, чтобы остаться в \(\mathbb{N}\) и не терять строгость округления), получаем гипотезу-вход
Левая часть \(12h + 72h^2\) — это точная целочисленная запись «энергии» повтора: линейный член \(12h\) отвечает за шаг вдоль линии, квадратичный член \(72h^2\) — за самоподобное удвоение масштаба на каждом уровне вложенности.
Естественно предположить (и ниже мы это докажем), что доминирует именно квадратичный член, и потому валидность повтора управляется корнем \(\sqrt{A}\), а не самим \(A\).
Теорема: кубический зажим¶
Теорема 7.1 (cubic_squeeze). Пусть \(A, h \in \mathbb{N}\) и выполнено \((7.1)\), то есть \(12(h + 6h^2) < A\). Тогда
Что доказано. Из полной стоимости \(12h + 72h^2 < A\) отбрасывается неотрицательный линейный член \(12h \ge 0\), и остаётся оценка на чистый квадратичный вклад. В Lean это одна строка omega: линейная арифметика над атомом \(h^2\), взятым как самостоятельная переменная. Округления нет, корень не извлекается — заключение остаётся целочисленным неравенством.
Почему так. Ключ в том, что \(12(h + 6h^2) = 12h + 72h^2\) и оба слагаемых неотрицательны. Строгое неравенство \((7.1)\) тем более сохраняется после удаления одного из положительных слагаемых слева: \(72h^2 \le 12h + 72h^2 < A\). Именно поэтому доказательство элементарно — вся работа сделана раскрытием скобок, а omega лишь закрывает тривиальную линейную арифметику.
Что это значит. Неравенство \((7.2)\) равносильно (в вещественной интерпретации) оценке
Высота повтора не может превзойти \(\sqrt{A/72}\).
Вывод. Валидный сегмент train'а имеет длину порядка \(\sqrt{A}\), а не \(A\) и тем более не \(\infty\). Аффинная линия индексов бесконечна, но реально проходимый двигателем её отрезок сжат до корня из активного масштаба. Это и есть cubic squeeze — кубическая стоимость зажимает квадратичный результат в квадратный корень.
Примечание. Мы сознательно работаем в целых числах и с \((7.2)\), а не с \((7.3)\). Вещественная форма с корнем — лишь интерпретация; load-bearing (несущее) утверждение, которое проверяет компилятор, — целочисленное. Никакой апелляции к иррациональностям и никакого скрытого округления в доказательство не входит.
Следствие: повтор ещё короче¶
Теорема 7.2 (cubic_squeeze_sq_lt). При том же входе \((7.1)\) имеем
Разбор. Это прямое ослабление зажима Теоремы 7.1: из \((7.2)\) и \(h^2 \le 72h^2\) получаем \(h^2 < A\); в Lean — have := cubic_squeeze hsq; omega. Формулировка \(h^2 < A\) удобнее для последующих склеек, поскольку убирает численный множитель \(72\) и даёт чистую оценку «квадрат высоты меньше масштаба». Содержательно она говорит то же: повтор атома крайне короток относительно \(A\).
Значение для каркаса: самоподобие и сжатие масштаба¶
Зажим \((7.3)\) — это количественная форма самоподобия двигателя. Каждый уровень повтора удваивает масштаб через квадратичный член \(72h^2\), поэтому число уровней, укладывающихся в бюджет \(A\), логарифмически-корневое, а не линейное. В геометрии фрактального слоя 13 это проявляется как сжатие масштаба \(P \to P^{1/3}\): кубическая стоимость повтора переводит один шаг вдоль линии в кубический корень по параметру, и повторный атом оказывается «крайне коротким».
Связь с общей картиной прямая. Топливо \(+1\) (шаг индекса вдоль линии) действительно бесконечно, но это не даёт двигателю бесконечного хода: валидный сегмент зажат. Это ещё одна грань асимметрии, зафиксированной в законе необратимости (05 Irreversibility): вверх линия тянется неограниченно, но вниз — по реально достижимым центрам — двигатель проходит лишь короткий отрезок \(O(\sqrt{A})\). Бесконечность носителя и конечность полезного хода — согласованная пара, как и «время не обратимо / всегда останавливается».
Примечание. Здесь нет редукции гипотезы близнецов к чему-либо — это атомарная, полностью проверенная лемма о геометрии повтора. Теорема 7.1 (
cubic_squeeze) и Теорема 7.2 (cubic_squeeze_sq_lt) компилируются чисто;#print axiomsпоказывает лишь стандартные[propext, Classical.choice, Quot.sound], безsorryAxи запрещённых аксиом. Мы не выдаём этот зажим за доказательство чего-то большего: он лишь ограничивает длину одного train'а. Открытых узлов внутри самой леммы нет.
Мост к следующей главе¶
Итак, вдоль одной аффинной линии повтор короток: не более \(\sqrt{A/72}\) центров. Но двигатель порождает не одну линию, а целый веер таких линий, и естественно спросить: что происходит, когда повторов и линий становится много — не возникает ли из симметрических сумм по этому вееру нетривиальное совпадение? Ответ даёт следующая глава: pigeonhole — пижонхол, принцип ящиков (см. словарь) — на симметрических суммах форсирует ограниченный аддитивный цикл (08 BK, exists_additive_cycle).
Короткий train ограничивает длину каждого повтора; ограниченный цикл ограничит их взаимную согласованность — и вместе они закрывают возможность вечного clean-recycling.