08. Ограниченный аддитивный цикл

← 07. Короткий train · Оглавление · 09. Factor-repeat rigidity →

Lean: EuclidsPath/Engine/BK.lean (exists_additive_cycle).

Где мы

В главе 07 мы зажали длину валидного train'а: даже вдоль бесконечной аффинной линии число реально достижимых центров коротко (cubic_squeeze). Топливо +1 неисчерпаемо, но валидный ход двигателя стеснён.

Теперь мы поворачиваем зажим в аддитивную плоскость: вместо длины одного хода спросим, сколько различных K-кратных комбинаций делителей может уместиться в ограниченном окне, прежде чем две из них неизбежно совпадут по сумме. Ответ — чистый pigeonhole, то есть пижонхол, принцип ящиков (см. словарь) — даёт нам первый структурный запрет на бесконтрольное накопление повторов.

Постановка: аддитивный цикл на K-мультимножествах

Зафиксируем конечное множество делителей (или центров) 𝒜 ⊆ [1, T], то есть каждый a ∈ 𝒜 удовлетворяет 1 ≤ a ≤ T. Параметр K ≥ 1 — порядок комбинации, «длина» аддитивного слова, которое двигатель складывает из элементов 𝒜.

Определение 8.1 (K-мультимножество). K-мультимножеством над 𝒜 называется мультимножество мощности K, все элементы которого лежат в 𝒜. Множество всех таких объектов в Lean/Mathlib записывается 𝒜.sym K (симметрическая K-степень). Порядок в мультимножестве не важен, повторы допускаются — это в точности «неупорядоченный выбор K элементов из 𝒜 с возвращением».

Каждому K-мультимножеству s ∈ 𝒜.sym K сопоставим его аддитивный вес — сумму элементов:

\[ \Sigma(s) \;=\; \sum_{x \in s} x \;=\; (s : \mathrm{Multiset}\ \mathbb{N}).\mathrm{sum}. \tag{8.1} \]

Определение 8.2 (нетривиальный аддитивный цикл). Нетривиальным аддитивным (евклидовым) циклом мы называем пару различных K-мультимножеств s ≠ t из 𝒜.sym K с равным весом:

\[ s \neq t, \qquad \Sigma(s) \;=\; \Sigma(t). \tag{8.2} \]

«Нетривиальность» здесь — именно s ≠ t: тривиальное равенство Σ(s) = Σ(s) ничего не стоит; содержательно то, что два разных способа сложить K делителей дают один и тот же итог.

Название «цикл» неслучайно. Равенство Σ(s) = Σ(t) при s ≠ t — это соотношение \(\sum_{x\in s} x - \sum_{y\in t} y = 0\), то есть нетривиальная целочисленная линейная зависимость (с коэффициентами ±1) между элементами 𝒜. Такая замкнутая аддитивная петля и есть «цикл» в аддитивной структуре, порождённой носителем.

Теорема: масса вынуждает цикл

Основной результат главы — контрапозиция леммы B_K (§VI, Лемма 6.1.1). Прямая лемма утверждает: если в 𝒜 ⊆ [1,T] нет нетривиального равенства K-сумм, то множество вынужденно мало, \(|𝒜| \ll_K T^{1/K}\). Нам, однако, нужна именно контрапозиция — то, что питает Fan-Cycle далее по цепи: как только комбинаторной массы достаточно, цикл обязан существовать.

Теорема 8.3 (exists_additive_cycle). Пусть \(\mathcal{A} \subseteq \mathbb{N}\) — конечное множество, \(K, T \in \mathbb{N}\), \(1 \le K\), и пусть

\[ 1 \le a \le T \quad \text{для всех } a \in \mathcal{A}, \qquad K \cdot T \;<\; |\,\mathcal{A}.\mathrm{sym}\ K\,|. \tag{8.3} \]

Тогда существуют \(s, t \in \mathcal{A}.\mathrm{sym}\ K\) такие, что \(s \neq t\) и \(\Sigma(s) = \Sigma(t)\) (8.2) — нетривиальный аддитивный евклидов цикл.

Условие K · T < |𝒜.sym K| — это порог массы: число различных K-мультимножеств превосходит число K·T возможных значений суммы. Всё доказательство — pigeonhole, без анализа, без распределения простых, без сита. Это делает результат атомарным законом двигателя, а не эвристикой.

Почему это верно: разбор доказательства

Доказательство в BK.lean устроено в три шага, и каждый честно отражает свою роль.

Шаг 1 — образ веса зажат в окне [K, K·T]. Пусть s ∈ 𝒜.sym K. По определению s — мультимножество мощности ровно K (в Lean это s.2 : (s : Multiset ℕ).card = K), все элементы которого лежат в 𝒜, а значит зажаты между 1 и T. Отсюда две границы:

\[ \Sigma(s) \;\ge\; K \cdot 1 \;=\; K \qquad\text{и}\qquad \Sigma(s) \;\le\; K \cdot T. \tag{8.4} \]

Нижняя граница — это Multiset.card_nsmul_le_sum (сумма K слагаемых, каждое ≥ 1, не меньше K); верхняя — Multiset.sum_le_card_nsmul (каждое ≤ T, значит сумма ≤ K·T). В коде это оформлено как

have hmaps : ∀ s ∈ 𝒜.sym K, (s : Multiset ℕ).sum ∈ Finset.Icc K (K * T)

то есть отображение веса Σ : 𝒜.sym K → ℕ действительно попадает в целочисленный отрезок Finset.Icc K (K*T).

Шаг 2 — окно значений тесное. Отрезок Finset.Icc K (K*T) содержит ровно K·T − K + 1 целых точек (Nat.card_Icc). При 1 ≤ K это не превосходит K·T. Гипотеза K·T < |𝒜.sym K| тогда даёт

\[ |\mathrm{Icc}(K,\,K{\cdot}T)| \;=\; K{\cdot}T - K + 1 \;\le\; K{\cdot}T \;<\; |\mathcal{A}.\mathrm{sym}\ K|. \tag{8.5} \]

В Lean это единственная арифметическая строка, закрываемая omega:

have hcard_lt : (Finset.Icc K (K * T)).card < (𝒜.sym K).card := by
  rw [Nat.card_Icc]; omega

Значений суммы строго меньше, чем K-мультимножеств.

Шаг 3 — pigeonhole. Отображение Σ переводит бо́льшее множество (все K-мультимножества) в меньшее (окно сумм). По принципу Дирихле оно не может быть инъективным: два разных прообраза склеиваются в один образ. Формально это Finset.exists_ne_map_eq_of_card_lt_of_maps_to, получающее ровно нужную пару:

obtain ⟨s, hs, t, ht, hne, heq⟩ :=
  Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard_lt hmaps

hne : s ≠ t и heq : Σ(s) = Σ(t) — это и есть нетривиальный аддитивный цикл. Доказательство завершается.

Примечание. Три шага соответствуют трём ингредиентам любого pigeonhole-аргумента: (1) отправить объекты в ящики (hmaps — вес попадает в окно), (2) посчитать, что ящиков мало (hcard_lt), (3) вывести коллизию (Finset.exists_ne_map_eq_of_card_lt_of_maps_to). Никакой из шагов не использует свойства простых чисел — работает любое 𝒜 ⊆ [1,T]. Именно поэтому это закон механизма, а не свойство конкретной арифметики.

Что это значит: ограничение порядка повторов

Содержательное следствие — граница на то, как долго носитель может расти «бесциклично». Переформулируем прямую лемму B_K как счётную оценку.

Предложение 8.4 (порог бесцикличности). Если \(\mathcal{A} \subseteq [1,T]\) не содержит нетривиального аддитивного цикла порядка \(K\) (в смысле Определения 8.2), то отображение веса \(\Sigma\) (8.1) инъективно на \(\mathcal{A}.\mathrm{sym}\ K\), откуда

\[ |\mathcal{A}.\mathrm{sym}\ K| \;\le\; |\mathrm{Icc}(K,\,K{\cdot}T)| \;=\; K{\cdot}T - K + 1 \;\le\; K{\cdot}T. \tag{8.6} \]

Поскольку \(|\mathcal{A}.\mathrm{sym}\ K|\) растёт как \(\binom{|\mathcal{A}| + K - 1}{K} \asymp |\mathcal{A}|^K / K!\), из (8.6) следует \(|\mathcal{A}|^K \lesssim K{\cdot}T\), откуда \(|\mathcal{A}| \ll_K T^{1/K}\). Это и есть \(|\mathcal{A}| \ll_K T^{1/K}\) из §VI. (Контрапозитивно: если \(|\mathcal{A}|^K \gg K \cdot T\), то по Теореме 8.3 цикл существует.)

Вывод. Избежать аддитивного цикла можно, лишь удерживая носитель радикально редким — не более чем порядка T^{1/K} элементов в окне [1,T]. Двигатель Евклида, напротив, вынужден накапливать делители на центрах вдоль хода; как только их набирается достаточно много относительно доступного окна значений, повтор сумм неизбежен. Через контрапозицию это переводится в структурный запрет: порядок повторов ограничен — нельзя бесконечно клонировать делительную конфигурацию, сохраняя все аддитивные веса различными.

В связке с невозможностью вечного двигателя — бесконечной строго убывающей цепи, главного запрещённого объекта программы (глава 01, no_infinite_descent) — это питает запрет вечного clean-recycling: если бы повторное использование делителей могло продолжаться без образования аддитивной петли, носитель рос бы, оставаясь бесцикличным, что противоречит порогу T^{1/K}. Цикл, гарантированный Теоремой 8.3 (exists_additive_cycle), — это точка, где «чистая» переработка топлива замыкается сама на себя и потому не может длиться вечно.

Примечание (граница результата). Теорема даёт существование цикла, но не его геометрию: она не говорит, какие именно делители в него входят, и не привязывает цикл к разностям центров. Эту привязку — что повтор делителя ℓ фиксирует ℓ ∣ (n₂ − n₁) — устанавливает уже следующая глава. Здесь мы честно фиксируем: Теорема 8.3 (exists_additive_cycle) — комбинаторный порог, а не структурная жёсткость; смешивать одно с другим нельзя.

Мост к следующему

Мы получили, что масса делителей вынуждает аддитивный цикл, и через контрапозицию — что порядок повторов ограничен окном T^{1/K}. Но чистое существование совпадающих сумм ещё не говорит, что повтор делителя влечёт периодичность попаданий вдоль хода.

В главе 09 (factor_repeat_rigidity, cross_side_fuel) мы придадим повтору жёсткость: если простой ℓ появляется делителем на двух центрах, он делит их разность, ℓ ∣ (n₂ − n₁). Ограниченный цикл этой главы и ригидность следующей вместе с коротким train'ом (глава 07) замкнут покрытие в конечное и короткое — превращая аддитивный запрет в геометрический.

---

← 07. Короткий train · Оглавление · 09. Factor-repeat rigidity →