23. Clean-boundary split¶
← 22. Residuals · Оглавление · 24. Boundary-декомпозиция →
В 22 Residuals мы закрыли остаточные Lean-леммы двигателя без обращения к плотности: конструктивный clean-старт выше любого \(N\) (carrier_nonempty_above), элементарное sink_is_twin (old-free сторона ниже \(A^2\) простая) и привязку clean_twin_above (при \(6N+1 < A\) twin-центр автоматически лежит выше \(N\)). Три эти факта дали нам инструменты, но не архитектуру: они говорят, чем оказывается остановка спуска, но не где именно спуску разрешено останавливаться. В этой главе мы наводим порядок в понятии остановки — и обнаруживаем скрытый разрыв, который до сих пор незаметно ломал редукцию.
Разрыв «sink-is-clean»¶
Начнём с наблюдения о конкретном сбое. В аудите спуска (RESULTS_descent_gap) обнаружилось, что евклидов спуск из clean-старта способен проскочить к малому twin-центру, который сам по себе не clean. Каноничный пример:
Пара \((107,109)\) — настоящие простые-близнецы, но центр \(m=18\) делится на простые \(2,3\), которые заведомо \(\le A\), а значит \(18 \notin \Omega_A\) (не old-free).
К такому центру теорема clean_twin_above неприменима: её посылка требует чистоты сторон относительно всех \(q \le A\), а здесь \(6m\pm1\) хоть и простые, но сам центр «загрязнён». Формально доказанная привязка «sink лежит выше \(M_0\)» рушится ровно потому, что мы позволили спуску финишировать на unclean-центре и всё равно назвали это sink.
Из интуиции разрыв устраняется одним ограничением: sink определяется только в clean-графе. Спуск к центру \(n \notin \Omega_A\) — это не остановка, а особый переход, который мы называем boundary-exit и отправляем в defect/old-peel ledger — бухгалтерию учёта нагрузок спуска (о леджерах см. словарь; главы 19–21). Малый unclean twin вроде \(18\) тогда честно классифицируется как boundary, а не как sink, и clean_twin_above применяется лишь там, где её посылки выполнены. Настоящая глава формализует доказуемую clean-часть этой конструкции.
Примечание. Разрыв был семантическим, а не арифметическим: обе стороны \((107,109)\) действительно простые. Ошибка состояла в том, что понятие «sink» молчаливо отождествлялось с «остановкой спуска», тогда как корректная остановка обязана быть внутри графа, на котором доказаны инварианты. Разграничение clean/boundary — это и есть ремонт этого молчаливого отождествления.
Определения графа¶
Зафиксируем порог просеивания \(A\) и работаем с центрами \(m \in \mathbb{N}\) (сторона \(6m-1\), \(6m+1\)). Основное свойство наследуется из 22, но здесь мы берём его натуральную форму.
Определение 23.1 (clean-центр). Центр \(m\) называется clean относительно \(A\), если ни один простой \(q \le A\) не делит ни одну из сторон:
В Lean это Clean (ℕ-версия; её ℤ-двойник — CleanZ из Residuals, мост между ними мы предъявим ниже).
Определение 23.2 (active-ребро). Ребро \(m \to n\) активно, если \(n\) — меньший центр-цель спуска:
В ActiveEdge носитель абстрактен: конкретный механизм (составная сторона \(6m+\sigma = a\,(6n+\varepsilon)\) с \(a > A\)) вынесен в OldPeel/cofactor и в active_descent_height из 22; здесь важно лишь, что active-ребро несёт строгое падение высоты \(n < m\).
Различие внутри active-рёбер и есть предмет главы:
Определение 23.3 (clean-ребро). \(\mathrm{CleanActiveEdge}\,A\,m\,n :\equiv \mathrm{Clean}\,A\,m \land \mathrm{Clean}\,A\,n \land \mathrm{ActiveEdge}\,A\,m\,n\) — оба конца clean.
Определение 23.4 (boundary-exit). \(\mathrm{BoundaryExit}\,A\,m\,n :\equiv \mathrm{Clean}\,A\,m \land \mathrm{ActiveEdge}\,A\,m\,n \land \neg\,\mathrm{Clean}\,A\,n\) — исток clean, цель не clean.
Boundary-exit — это ребро, покидающее clean-граф. Оно не sink: это вход в defect-ledger, где им занимаются old-peel и регенерация. Именно сюда уходит переход \(18 \to \dots\) из разрыва выше.
Дихотомия active-ребра¶
Первая теорема — полная и безусловная классификация каждого active-ребра, выходящего из clean-центра.
Теорема 23.5 (active_edge_clean_or_boundary). Если \(m\) clean и есть active-ребро \(m \to n\), то это ребро либо clean, либо boundary-exit:
Доказательство тривиально по закону исключённого третьего для предиката \(\mathrm{Clean}\,A\,n\): если \(n\) clean — левая ветвь, иначе — правая. Содержательна не сложность, а полнота: третьего исхода у active-ребра из clean-центра нет. Это значит, что граница clean-графа замкнута — всякая стрелка, выходящая наружу, ровно одна из двух: остаётся внутри (clean-edge) или пробивает границу (boundary). Именно эта дихотомия позволяет строго отделить «внутреннюю работу» спуска от «выхода на границу», где начинает действовать другой аппарат.
Примечание. Заметим, что дихотомия формулируется от истока \(m\) (он обязан быть clean), но исход определяется свойством цели \(n\). Асимметрия неслучайна: clean-граф — это область, где мы умеем доказывать инварианты; выходя из неё, мы теряем гарантии на \(n\) и обязаны передать управление ledger'у.
Clean-sink есть twin¶
Теперь — корректное понятие остановки.
Определение 23.6 (clean-sink). \(m\) — clean-sink, если \(m\) clean и у него вообще нет active-ребра:
Ключевое слово — «вообще нет»: unclean-цель, к которой ведёт boundary-ребро, не считается sink. Спуск, упирающийся в \(18 \to (107,109)\), active-ребро имеет (переход существует), поэтому он не clean-sink, а boundary-exit. Так разрыв «sink-is-clean» устранён на уровне определения.
Теорема 23.7 (clean_sink_is_twin, исправленная Лемма 3.1). Если \(m\) clean, обе стороны \(6m-1,\,6m+1 \ge 2\) и обе \(< A^2\), и \(m\) — clean-sink, то \(m\) — twin-центр:
Доказательство опирается на sink_is_twin из 22: clean-сторона ниже \(A^2\) обязана быть простой, потому что её минимальный простой делитель либо \(\le A\) (запрещено чистотой), либо \(> A\), и тогда кофактор тоже \(> A\), откуда \(6m\pm1 > A^2\) — противоречие.
Заметим тонкость реализации: посылка \(\mathrm{CleanSink}\) содержит «нет active-ребра», но напрямую в доказательстве используется только чистота (\(\mathrm{hsink}.1\)). Отсутствие ребра здесь работает не как арифметический факт, а как семантическая гарантия: раз остановка легальна (внутри clean-графа) и ни одна сторона не составная относительно \(q \le A\), обе стороны простые — это и есть twin. Old-free ниже \(A^2 \Rightarrow\) простое; чётность и делимость на \(3\) элементарны и уже поглощены oldfree_below_sq_prime.
Полный исход clean-центра¶
Сведём дихотомию рёбер и понятие sink в единую классификацию.
Теорема 23.8 (clean_center_outcome, §5). Для любого clean-центра \(m\) выполнено ровно одно из четырёх:
Доказательство — вложенный разбор случаев: если \(m\) уже twin, готово; иначе смотрим, есть ли у \(m\) хоть какое-то active-ребро. Если есть — применяем Теорему 23.5 (active_edge_clean_or_boundary) и попадаем в clean-edge или boundary. Если ни одного active-ребра нет — по определению это clean-sink.
Значимость теоремы в том, что она корректно отсекает unclean малый twin от sink: центр \(18\), будучи истоком boundary-exit-ребра, оседает в третьей ветви (boundary), а не в первой (twin) и не в четвёртой (sink). Раньше он ошибочно проваливался в «sink», ломая привязку по высоте; теперь классификация не пускает его туда.
Примечание. Четыре ветви — это не выбор, а исчерпание: twin (терминал-успех), clean-edge (продолжаем спуск внутри графа), boundary (передаём управление defect-ledger), clean-sink (остановились чисто \(\Rightarrow\) twin по Теореме 23.7). Первая и четвёртая ветви — «выходы вверх» к результату; вторая — внутренняя динамика; третья — единственный канал, уводящий нагрузку прочь из clean-графа.
Clean-sink лежит выше \(M_0\)¶
Осталось связать корректную остановку с высотой — то, ради чего вводилось ограничение «sink только в clean».
Теорема 23.9 (clean_sink_above, §4). Если \(6M_0+1 < A\), \(m \ge 1\), \(m\) clean и twin, то \(m > M_0\):
Это мост к уже доказанной Residuals.clean_twin_above. Единственная работа здесь — перенос ℕ-делимости в ℤ-делимость сторон: равенства
(первое требует \(1 \le 6m\) для корректного Nat.cast_sub) позволяют переписать посылку hcl из натуральной чистоты в целочисленную, после чего срабатывает clean_twin_above.
Содержательно она говорит: простое \(6m-1\) обязано быть \(> A\) (иначе старое простое делило бы свою сторону, нарушая clean), а \(A > 6M_0+1\), откуда \(6m-1 > 6M_0+1\) и \(m > M_0\). Теперь эта импликация безопасна именно потому, что мы гарантировали чистоту \(m\): на unclean-центре \(18\) она бы не применилась, и мы больше не пытаемся её туда применить.
Честная граница: clean-граф не самодостаточен¶
Здесь мы обязаны быть точны и не выдать редукцию за доказательство. Формализованная clean-часть — Теоремы 23.5 (active_edge_clean_or_boundary), 23.7 (clean_sink_is_twin), 23.8 (clean_center_outcome), 23.9 (clean_sink_above) — доказана полностью, стандартными аксиомами, без sorry. Но она описывает лишь внутренность и границу clean-графа, а не его замкнутость. И измерения показывают, что граф далеко не замкнут.
Числа RESULTS_clean_graph: 59% clean-центров имеют все свои active-рёбра в boundary — то есть у большинства clean-центров каждый выход из графа пробивает границу, ведя к unclean-цели. Это означает, что clean-граф не самодостаточен: спуск, стартовавший чисто, почти всегда вынужден покинуть clean-область, и почти вся нагрузка редукции уходит в ветвь BoundaryExit из clean_center_outcome.
Вывод. Весь остаток программы концентрируется в единственном открытом входе — именованном 🔴-утверждении, которого не хватает до цели (см. словарь): boundary-состояние обязано регенерировать — порождать корректного преемника (clean-возврат либо шаг defect-ledger), а не быть висячим терминалом. В движке это гипотеза
Подчеркнём прямо: (H) не доказана. Это явная гипотеза, а не лемма. Clean-часть честно локализовала трудность — она сузила весь открытый узел до одного структурного утверждения о boundary-выходах, — но не закрыла его.
Примечание. Разрыв «sink-is-clean» и число \(59\%\) — две стороны одного факта. Пока мы ошибочно считали unclean twin sink'ами, граф казался почти замкнутым: спуск «останавливался» повсюду. Как только остановка ограничена clean-центрами, обнаруживается, что \(59\%\) мнимых остановок были на самом деле boundary-выходами. Ремонт не создал нагрузку на boundary — он сделал её видимой.
План закрытия. (H) — не счётная и не распределительная гипотеза; она в духе regenerate из 20 NOPSL и Леммы 6.1 о регенерации из 21 Regeneration.
Естественно предположить, что boundary-выход \(m \to n\) с \(n \notin \Omega_A\) по определению \(\Omega_A\) даёт простой делитель \(q \le A\), \(q \ge 5\) одной из сторон \(n\) — то есть old-peel edge, — и что old-peel ledger 19–21 замыкается на этот делитель с падением высоты. Тогда (H) свелась бы к уже изученному regenerate, и вся программа замкнулась бы на один структурный факт регенерации boundary. Предъявить это замыкание строго — задача следующего шага.
Итог раздела. Итак, мы разделили граф на чистую внутренность (доказано) и границу (открыто), и локализовали весь остаток в boundary_exit_regenerates. Но boundary-выходов бесконечно много и на всех масштабах \(A\); отдельные локальные регенерации не дают глобального вывода, пока мы не соберём их в один инвариант, действующий сразу на всём дереве родословных. Как склеить локальную дихотомию clean/boundary в глобальное утверждение о неограниченности twin-центров — предмет [24 Global node], к которому мы переходим.