25. Rigid closure: спуск без цикла¶

← 24. Boundary-декомпозиция · Оглавление · 26. Separating scale →

Источник: Engine/RigidClose.lean (namespace EuclidsPath.RigidClose; стандартные аксиомы, без sorry в ядре — открытым остаётся один конструктивный вход). Числа: кофактор 100% на 307010 случаях.

В предыдущей главе 24 boundary мы разложили активную сторону на граничные слои и убедились, что делимость катча всегда приходит с конкретным делителем — граница не бывает «пустой». Теперь мы возьмём этот делитель и покажем, что он не просто существует, а строит следующий, меньший центр, — и что этого одного факта достаточно, чтобы замкнуть всю конструкцию спуска без обращения к циклу и без ветки engine. Иначе говоря, мы заменяем прежний аргумент «поток без стоков ⟹ directed cycle ⟹ двигатель Евклида ⟹ ⊥» на прямое утверждение о well-foundedness.

Мотивация: почему цикл был лишним¶

Напомним прежнюю логику замыкания (см. [19 old-peel]). Если каждый не-twin центр имеет исходящее ребро спуска, то поток old-peel не имеет стоков; по графовой лемме такой поток замыкается в directed cycle; а цикл — это и есть rigid-двигатель, запрещённый EPMI (двигатель — главный запрещённый объект программы, см. словарь). Схема рабочая, но в ней три отдельных нетривиальных звена: (i) построение цикла из отсутствия стоков, (ii) отождествление цикла с двигателем, (iii) rigid-подпись цикла (аудит §13.D).

Наблюдение, снимающее все три звена, элементарно. Ребро спуска не просто «уходит куда-то» — оно строго уменьшает высоту. А в такой ситуации directed cycle невозможен по совершенно тривиальной причине: высота не может вернуться к исходному значению, если каждый шаг её строго уменьшает. Значит, вместо того чтобы строить цикл и приводить его к противоречию, естественно предположить, что достаточно сослаться на фундированность $\mathbb{N}$ напрямую. Строгое падение высоты само по себе исключает бесконечный спуск — а с ним и цикл, и всю ветку engine.

Эта глава формализует данное наблюдение в виде абстрактного «жёсткого» (rigid) графа с высотой и доказывает, что в нём достижение twin следует из одного лишь свойства регенерации — сильной индукцией по высоте.

Определение: граф с высотой¶

Абстрагируемся от арифметики. Всё, что нужно от механизма спуска, — это высота, отношение перехода и признак стока.

Определение 25.1 (HeightGraph). Жёсткий граф с высотой над типом состояний $\sigma$ — это набор

\[ G = \bigl(\mathrm{height} : \sigma \to \mathbb{N},\; \mathrm{Twin} : \sigma \to \mathrm{Prop},\; \mathrm{Step} : \sigma \to \sigma \to \mathrm{Prop}\bigr), \]

подчинённый единственной аксиоме строгого падения:

\[ \forall\, s\, t,\quad \mathrm{Step}\,s\,t \;\Longrightarrow\; \mathrm{height}\,t < \mathrm{height}\,s. \]

В Lean это структура HeightGraph с полем step_drops : ∀ {s t}, Step s t → height t < height s. Поле Twin — предикат корректного стока (в приложении — «$t$ есть twin-центр»); поле Step — отношение «есть ребро спуска» (в приложении — old-peel или active edge).

Единственный содержательный вход в конструкцию мы выделяем в отдельное свойство.

Определение 25.2 (Regenerates). Граф $G$ регенерирует, если каждое не-twin состояние имеет нисходящего преемника:

\[ \mathrm{Regenerates}(G) \;:\equiv\; \forall\, s,\; \neg\,\mathrm{Twin}\,s \;\Longrightarrow\; \exists\, t,\; \mathrm{Step}\,s\,t. \]

В Lean это def Regenerates (G : HeightGraph σ) : Prop. Заметим асимметрию нагрузки: аксиома step_drops про падение высоты дана «бесплатно» самой структурой (она встроена в определение ребра), тогда как Regenerates — единственное свойство, которое придётся доказывать в приложении. Вся дальнейшая теорема живёт над этими двумя данностями и больше ничего не требует.

Основная теорема: достижение twin без цикла¶

Теперь центральное утверждение главы.

Теорема 25.3 (reaches_twin). Если $G$ регенерирует, то из любого старта достигается twin:

\[ \mathrm{Regenerates}(G) \;\Longrightarrow\; \forall\, s : \sigma,\; \exists\, t,\; \mathrm{Twin}\,t. \]

Разберём, что здесь доказано и почему именно так. Доказательство — сильная индукция по высоте старта (Nat.strong_induction_on). Вспомогательное утверждение: $$\mathrm{key} : \forall\, n : \mathbb{N},\; \forall\, s,\; \mathrm{height}\,s = n \;\Longrightarrow\; \exists\, t,\; \mathrm{Twin}\,t.$$ Фиксируем $n$ и гипотезу индукции ih, дающую заключение для всех строго меньших высот. Для состояния $s$ высоты $n$ разбираем случай:

если $\mathrm{Twin}\,s$ — сток уже найден, берём $t := s$;
иначе hregen даёт преемника $t$ с $\mathrm{Step}\,s\,t$; по step_drops имеем $\mathrm{height}\,t < \mathrm{height}\,s = n$, и применение ih к высоте $\mathrm{height}\,t$ замыкает шаг.

Почему это работает, а цикл был не нужен. Индукция не строит никакой путь и не рассматривает никаких циклов. Она просто утверждает: множество достижимых высот — подмножество $\mathbb{N}$, а $\mathbb{N}$ фундирован. Не-twin состояние обязано сойти на строго меньшую высоту, а строго убывать вечно в $\mathbb{N}$ нельзя.

Твёрдость (rigidity) графа — то, что каждый шаг строго роняет высоту, — превращает «нет стоков» из повода строить цикл в прямое противоречие с фундированностью. Ветку «цикл ⟹ engine» мы не отбрасываем как ложную — мы показываем, что она логически избыточна: то, ради чего она вводилась (невозможность бесконечного невозвращения к twin), уже содержится в аксиоме падения.

Примечание. Формулировка $\forall s,\ \exists t,\ \mathrm{Twin}\,t$ намеренно слабее, чем «из $s$ достижим twin по $\mathrm{Step}$-пути»: она утверждает лишь существование twin-стока во всём графе, что и требуется для финального противоречия (в приложении «twin существует на каждой высоте» — это уже теорема о бесконечности близнецов на данном масштабе). Усиление до конкретного пути тривиально извлекается из той же индукции, но для замыкания не нужно.

Невозможность цикла как отдельная лемма¶

Ту же фундированность мы фиксируем и в явном, «графовом» виде — как прямую замену прежнего rigid-цикла.

Теорема 25.4 (no_cycle). В графе с строго убывающей высотой directed cycle не существует. Точнее, для любой цепи $z : \mathbb{N} \to \sigma$

\[ \bigl(\forall\, k,\; \mathrm{Step}\,(z\,k)\,(z\,(k{+}1))\bigr) \;\Longrightarrow\; \bot. \]

Доказательство — одна строка: из цепи $z$ получаем последовательность высот $k \mapsto \mathrm{height}\,(z\,k)$, которая по step_drops строго убывает на каждом шаге, а OldPeel.old_peel_terminates (то же ядро, что no_infinite_engine_descent из [19 old-peel]) утверждает, что строго нисходящей бесконечной цепи в $\mathbb{N}$ не бывает. То есть no_cycle — это переупаковка уже доказанной невозможности двигателя: мы не доказываем её заново, мы указываем, что «бесконечная $\mathrm{Step}$-цепь» есть частный случай «бесконечного строгого спуска».

Примечание. Разница с прежней схемой чисто логическая, но существенная для аудита: раньше невозможность цикла была следствием отождествления цикла с rigid-двигателем (звено §13.D, требующее подписи). Здесь она — определение twёрдого графа. Rigid-подпись как отдельный вход исчезает: она уже вшита в step_drops.

Целевой центр строится алгеброй¶

Осталось одно: показать, что абстрактное ребро Step в арифметическом приложении действительно строится, а не постулируется. Именно тут прежде пряталась дыра — из «делитель $q$ существует» не следует автоматически, что частное есть валидный меньший центр нужной формы $6t'+\eta'$. Эту конструкцию мы доказываем алгеброй.

Теорема 25.5 (cofactor_is_center). Пусть $t,q,\eta \in \mathbb{Z}$, причём $t \ge 1$, $\eta \in \{+1,-1\}$, простой делитель $q \ge 5$ взаимно прост с $6$ (то есть $q \bmod 6 \in \{1,5\}$) и $q \mid 6t+\eta$. Тогда существуют $t',\eta'$ такие, что

\[ \eta' \in \{+1,-1\},\qquad 6t'+\eta' = \frac{6t+\eta}{q},\qquad 0 \le t' \;<\; t. \]

Это ключевая содержательная лемма главы: она превращает делимость в состояние. Разберём почему заключение именно такое.

Пишем $6t+\eta = q\cdot c$, откуда $(6t+\eta)/q = c$ (целочисленное деление точно, Int.mul_ediv_cancel_left). Дальше — три наблюдения.

Кофактор взаимно прост с $6$. Из $6t+\eta = qc$ по модулю $6$: $\eta \equiv (q \bmod 6)\cdot(c \bmod 6) \pmod 6$. Перебор конечного числа случаев $q\bmod 6 \in\{1,5\}$, $\eta\in\{\pm1\}$, $c\bmod 6\in\{0,\dots,5\}$ (в Lean — rcases … <;> omega) оставляет ровно $c \bmod 6 \in \{1,5\}$. Содержательно: и левая часть $6t+\eta$, и множитель $q$ лежат вне классов $2,3,4\pmod 6$ (взаимно просты с $6$); значит и второй множитель $c$ обязан лежать в $\{1,5\}\pmod 6$ — иначе произведение потеряло бы взаимную простоту с $6$. Это и есть то, что $c$ имеет форму центра $6t'\pm1$.
Кофактор положителен. Поскольку $6t+\eta > 0$ (при $t\ge1$, $\eta\ge-1$) и $q>0$, из $qc = 6t+\eta$ следует $c>0$ (nlinarith). Значит $t' \ge 0$ — центр не «уходит в ноль».
Строгое падение. Из $q \ge 5$ и $qc = 6t+\eta \le 6t+1$ получаем $5c \le 6t+1$ (nlinarith), откуда $c < 6t/5 + \tfrac15$, и после раскладки $c = 6t'\pm1$ выходит $t' < t$ (omega). Разбор двух случаев $c\bmod6=1$ (тогда $\eta'=+1$, $t'=(c-1)/6$) и $c\bmod6=5$ (тогда $\eta'=-1$, $t'=(c+1)/6$) завершает построение.

Таким образом кофактор $c=(6t+\eta)/q$ всегда оказывается корректным центром $6t'+\eta'$ строго меньшей высоты $t'<t$. Делимость, доставленная границей из 24 boundary, автоматически конвертируется в ребро Step жёсткого графа — падение высоты обеспечено пунктом 3, форма центра — пунктом 1, неотрицательность — пунктом 2.

Примечание (числа). Утверждение проверено эмпирически на 307010 случаях с попаданием 100%: во всех проверенных катчах кофактор действительно оказался валидным меньшим центром формы $6t'+\eta'$. Это не заменяет доказательство (оно чисто алгебраическое и уже полное), но подтверждает, что лемма покрывает реальный поток old-peel без исключений — «дыр по краям» диапазона нет.

Честная редукция: что построено, а что остаётся входом¶

Соберём баланс доказанного и открытого. Дихотомия регенерации (regeneration_dichotomy, 21 regeneration) для центра $t$ даёт один из трёх элементарных классов: Twin t; либо (¬OldFree) old-peel делитель $q$; либо (OldFree, не twin) составная активная сторона. Чтобы получить Regenerates, из каждого правого случая нужно построить конкретное ребро вниз — то есть предъявить $t' < t$ формы центра.

Здесь важно провести честную границу.

Падение высоты $t'<t$ доказано отдельно в обоих случаях: active_descent_height (составная сторона) и old_peel_height_drop (old-peel).
Форма центра $6t'+\eta'$ доказана ровно теперь — теоремой 25.5 (cofactor_is_center). Именно она закрывает нетривиальный переход «делитель $q\mid 6t+\eta$» $\Rightarrow$ «существует центр $t'$ формы $6t'+\eta'$», который не следует из одной делимости автоматически (кофактор мог бы быть кратен $2$ или $3$ — лемма показывает, что не может).

С учётом этого мы фиксируем оставшийся вход — в домовом смысле: честно названное недоказанное звено (см. словарь) — как честную редукцию, а не выдаём её за доказательство:

Теорема 25.6 (regenerates_needs_target_center). Если для каждого не-twin центра построено ребро вниз, то граф регенерирует:

\[ \bigl(\forall\, t,\; \neg\,\mathrm{Twin}\,t \Rightarrow \exists\, t',\; \mathrm{Step}\,t\,t'\bigr) \;\Longrightarrow\; \mathrm{Regenerates}(G). \]

Эта теорема тавтологична по построению (в Lean её тело — просто build_target), и именно в этом её ценность: она явно называет единственный оставшийся конструктивный вход. Не «где-то есть дыра», а точно: нужно, чтобы у каждого не-twin центра делитель порождал валидный меньший центр. Половину этого входа — форму и падение — мы уже закрыли (теорема 25.5 (cofactor_is_center) плюс height-drop леммы); остаётся собрать это в единое build_target над полной дихотомией, то есть удостовериться, что дихотомия действительно доставляет делитель во всех не-twin случаях без несclassifiable терминала.

Гипотеза и план закрытия. Гипотеза: для каждого не-twin центра $t$ дихотомия (regeneration_dichotomy) доставляет либо old-peel делитель $q\ge5$, $q\mid 6t\pm1$, либо составную сторону с большим делителем — то есть в любом случае существует $q$, к которому применима cofactor_is_center.

План: (i) из not_oldfree_gives_peel извлечь $q$ в случае $t\notin\Omega_A$; (ii) из composite_oldfree_has_big_divisor — в active-случае; (iii) применить теорему 25.5 (cofactor_is_center) к каждому $q$, получив $\mathrm{Step}\,t\,t'$; (iv) подставить результат как build_target в теорему 25.6 (regenerates_needs_target_center) и через теорему 25.3 (reaches_twin) замкнуть на существование twin.

Узел, который здесь остаётся по-настоящему открытым, — не арифметика ребра (она построена), а полнота дихотомии на нужном множестве центров: что fan-in/Hall не вводит скрытый несclassifiable класс. Именно этот вход и переезжает в следующую главу.

Где мы теперь и мост дальше¶

Итог главы. Строгое падение высоты делает цикл логически лишним. Мы заменили связку «нет стоков ⟹ directed cycle ⟹ rigid-двигатель ⟹ ⊥» на прямую сильную индукцию по высоте (теорема 25.3 (reaches_twin)), а невозможность цикла оставили лишь как переупаковку уже доказанной фундированности (теорема 25.4 (no_cycle)). Ветка engine и rigid-подпись как отдельные входы исчезли.

Более того, единственное арифметически нетривиальное звено — что делитель порождает валидный меньший центр — теперь доказано алгеброй (теорема 25.5 (cofactor_is_center), 100% на 307010 случаях), а оставшийся вход честно локализован в одной тавтологической редукции — теореме 25.6 (regenerates_needs_target_center).

Что осталось незакрытым, мы назвали явно: полнота дихотомии, то есть отсутствие несclassifiable терминала на carrier-scale. Это уже не вопрос о ребре одного центра, а вопрос о множестве родословных, сходящихся в ограниченное множество центров, — тот самый fan-in/Hall.

В следующей главе [26 separating scale] мы атакуем именно этот counting-узел: покажем, что на масштабе разделения $P_A > 6X_A+1$ активный фактор становится меньше примориала, coarse-паспорт становится exact, и ProductHall закрывается чистой арифметикой — сужая трихотомию до одной ветви и превращая «полноту дихотомии» из надежды в проверяемое разделяющее неравенство.

← 24. Boundary-декомпозиция · Оглавление · 26. Separating scale →