09. Factor-repeat rigidity

← 08. Ограниченный цикл · Оглавление · 10. survivor ⇒ twin →

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

Остаётся понять, насколько жёстко устроен каждый отдельный повтор делителя — и здесь мы переходим от статистики (сколько повторов вообще возможно) к геометрии одного повтора (где именно он обязан стоять). Настоящая глава показывает: повторное использование делителя вдоль линейного train'а ригидно — его позиции привязаны к шагу арифметической прогрессии, а не свободны.

Lean-источник: EuclidsPath/Engine/Cycle.lean (factor_repeat_rigidity, cross_side_fuel).

Постановка: делитель на линейном train'е

Напомним конфигурацию, унаследованную от carrier'а 02. Носитель двойки и descent'а 04. Спуск.

Центры двигателя (двигатель — запрещённый бесконечный спуск, см. словарь) вдоль одной аффинной линии образуют арифметическую прогрессию: значение, «сканируемое» простым делителем в точке с координатой \(n\), имеет вид

\[ V(n) = N_0 + q\cdot n, \tag{9.1} \]

где \(N_0\) — базовое смещение (сдвиг линии), а \(q\) — шаг train'а (общий множитель координаты). Это линейный train в терминологии программы: одна прямая в \(\mathbb{Z}\), параметризованная целым \(n\), вдоль которой мы спрашиваем, какие простые её делят и на каких центрах.

Естественно предположить, что «большой» делитель, однажды использованный, не может дёшево повторяться: если он делит \(V(n)\) на двух разных центрах, эти центры не свободны друг относительно друга. Именно это утверждение мы делаем точным.

Примечание. Слово «большой» здесь конкретизируется условием взаимной простоты \(\gcd(\ell,q)=1\). Все активные делители в clean-core программы превосходят порог \(A\) (см. boundary-exit из 06. Нет хода назад), тогда как шаг \(q\) построен из уже удалённой, «малой» части; поэтому взаимная простота \(\ell\) и \(q\) — не искусственное допущение, а структурное свойство конфигурации.

Определение (ригидность повтора)

Определение 9.1 (ригидность повтора). Пусть простое (или, шире, целое) \(\ell\) делит значения train'а на двух центрах \(n_1, n_2\):

\[ \ell \mid N_0 + q\,n_1,\qquad \ell \mid N_0 + q\,n_2, \]

и пусть \(\ell\) взаимно просто с шагом, \(\mathrm{IsCoprime}(\ell,q)\). Мы говорим, что повтор делителя \(\ell\) ригиден, если разность центров кратна \(\ell\):

\[ \ell \mid (n_2 - n_1). \]

Иначе говоря, множество центров, на которых \(\ell\) «срабатывает», само является арифметической прогрессией с шагом \(\ell\) по координате \(n\).

Теорема о ригидности повтора

Теорема 9.2 (factor_repeat_rigidity). Для целых \(\ell, q, N_0, n_1, n_2\)

\[ \ell \mid N_0 + q\,n_1 \ \wedge\ \ell \mid N_0 + q\,n_2 \ \wedge\ \mathrm{IsCoprime}(\ell,q) \ \Longrightarrow\ \ell \mid (n_2 - n_1). \tag{9.2} \]

Разбор доказательства. Оно элементарно и полностью конструктивно; в Lean это три строки. Вычитая одно условие делимости из другого, получаем, что \(\ell\) делит разность значений train'а, а базовое смещение \(N_0\) сокращается:

\[ (N_0 + q\,n_2) - (N_0 + q\,n_1) = q\,(n_2 - n_1), \]

откуда \(\ell \mid q\,(n_2 - n_1)\). Теперь работает взаимная простота: \(\ell\) делит произведение \(q\cdot(n_2-n_1)\), но не имеет общих множителей с \(q\), поэтому вся «делимость» переносится на второй сомножитель — \(\ell \mid (n_2 - n_1)\). В Lean этот шаг — ровно hcop.dvd_of_dvd_mul_left hd (лемма Евклида в форме IsCoprime).

Почему так. Ключ — сокращение \(N_0\) при вычитании. Линейность train'а означает, что делимость \(\ell \mid V(n)\) есть условие на \(n\) по модулю \(\ell\): \(q\,n \equiv -N_0 \pmod{\ell}\). Поскольку \(q\) обратимо по модулю \(\ell\) (взаимная простота), это уравнение имеет единственный класс вычетов решений \(n \bmod \ell\). Два решения \(n_1, n_2\) поэтому лежат в одном классе — их разность кратна \(\ell\). Условие \(\gcd(\ell,q)=1\) здесь не техническое: без него \(q\) необратимо, класс решений может быть пустым или «размазанным», и ригидность рушится.

Что это значит. Большой делитель «привязывает» свои повторы к решётке шага \(\ell\). На отрезке train'а длины \(L\) (координата \(n\) пробегает интервал длины \(L\)) простое \(\ell > A\) может повториться не более чем \(\lfloor L/\ell\rfloor + 1\) раз. Так делимость превращается в счётный ресурс: чем крупнее делитель, тем реже он способен возвращаться. Это и есть fuel-law в её чистой форме — «топливо» повтора расходуется пропорционально размеру делителя.

Примечание. Ригидность объясняет, почему запрет «вечного повтора» из 08. Ограниченный цикл замыкается. BK ограничивает число повторов через аддитивный цикл; Теорема 9.2 (factor_repeat_rigidity) ограничивает их расположение — каждый повтор большого делителя стоит на фиксированном шаге \(\ell\). Вместе с cubic squeeze из 07. Короткий train, зажимающим саму длину валидного сегмента train'а до \(L < \sqrt{A/72}\), это делает покрытие большими делителями конечным и коротким: короткий отрезок, редкие повторы, счётный бюджет.

Перенос двойки между сторонами (cross-side fuel)

Ригидность повтора описывает один линейный train. Но звено двигателя — это евклидово уравнение \(XY - ZW = 2\) (rank-\((3,3)\) форма abv + 2 = qrs, см. 05. Необратимость), у которого две стороны, и константа \(+2\) живёт именно в связке между ними. Второй закон этой главы отслеживает, как делимость переносится через двойку с одной стороны звёздного прямоугольника на противоположную.

Определение 9.3 (fuel-law, делимостная форма). Рассмотрим простое \(p\), делящее линейные формы на противоположных сторонах, различающиеся ровно на константу \(2\) (наследие \(+2\) det-формы). В чистом виде: пусть при параметрах \(a, c, \alpha, \beta\) выполнено

\[ p \mid a\,\alpha + c,\qquad p \mid a\,\beta + c - 2. \]

Первое — попадание \(p\) на сторону \(\alpha\), второе — на противоположную сторону \(\beta\), сдвинутую на \(-2\) двойкой уравнения.

Теорема 9.4 (cross_side_fuel). При этих условиях

\[ p \mid \bigl(a\,(\beta - \alpha) - 2\bigr). \tag{9.3} \]

Разбор доказательства. Механика та же, что и у ригидности: вычитаем и сокращаем свободный член \(c\). Именно,

\[ (a\,\beta + c - 2) - (a\,\alpha + c) = a\,(\beta - \alpha) - 2, \]

и левая часть делится на \(p\) как разность двух кратных \(p\). В Lean это dvd_sub h2 h1, переписанное через тождество ring. Дополнительной взаимной простоты здесь не требуется — двойка не сокращается и остаётся явно в правой части.

Почему так и что это значит. В отличие от Теоремы 9.2 (factor_repeat_rigidity), где после сокращения оставалось «чистое» \(q\,(n_2-n_1)\) и работал евклидов перенос, здесь после сокращения \(c\) остаётся жёсткий след \(-2\). Поэтому Теорема 9.4 (cross_side_fuel) даёт не сравнение \(a(\beta-\alpha)\equiv 0\), а сдвинутое сравнение

\[ a\,(\beta - \alpha) \equiv 2 \pmod{p}. \]

Двойка евклидова уравнения «путешествует» между сторонами: делитель \(p\), чтобы встать сразу на обе стороны звёздного прямоугольника, обязан согласовать межстороннюю разность \(\beta-\alpha\) с \(2/a \bmod p\). Это и есть перенос топлива \(+2\) поперёк сторон (детально механизм переноса разбирается в 11. Блочное ядро и синтезируется как «первый закон — сохранение двойки»).

Вывод. Геометрически (см. doc-string в Cycle.lean) это форма условия \(p \mid 2 + a\,q\,(\beta-\alpha)\) на det-форме звёздного прямоугольника: две противоположные стороны не могут независимо «поймать» один и тот же \(p\) — их положения связаны через двойку.

Примечание. Обе теоремы — 9.2 и 9.4 — имеют одну и ту же элементарную сердцевину: «вычесть и сократить свободный член». Разница в остатке: у Теоремы 9.2 (factor_repeat_rigidity) он нулевой (после чего добивает взаимная простота), у Теоремы 9.4 (cross_side_fuel) он равен \(-2\) (и остаётся видимым как перенос двойки). Первая ограничивает повтор внутри стороны, вторая связывает разные стороны. Обе — про то, что делимость на линейной структуре не свободна, а привязана к шагу и к константе \(+2\).

Статус

• 🟢 Строго и проверено компилятором. Обе теоремы — Теорема 9.2 (factor_repeat_rigidity) и Теорема 9.4 (cross_side_fuel) — доказаны в EuclidsPath/Engine/Cycle.lean элементарно (делимость + взаимная простота), без sorry и без нестандартных аксиом. Это твёрдые леммы-инструменты: жёсткость расположения повтора и межстороннее сравнение \(a(\beta-\alpha)\equiv 2\).
• 🔴 Открыто (на уровне применения). Локальная ригидность одного делителя не даёт сама по себе глобального non-cover: остаётся показать, что суммарный бюджет всех больших делителей на коротком train'е строго меньше carrier'а. Явная гипотеза: на каждом масштабе число центров, покрытых старыми/большими делителями, ограничено сверху как \(\sum_{\ell > A} (\lfloor L/\ell\rfloor + 1)\), и эта сумма по короткому сегменту (\(L < \sqrt{A/72}\) из 07. Короткий train) остаётся ниже размера carrier'а. План закрытия: соединить счётную оценку повторов (эта глава) с carrier-оценкой и bad-upper из 10. survivor ⇒ twin, передав их дальше блочному мосту 11. Блочное ядро. Здесь мы не выдаём ригидность за non-cover — она лишь делает бюджет покрытия конечным и счётным, а не бесконечным.

Мост к следующей главе

Итак, повтор большого делителя ригиден, а двойка ригидно переносится между сторонами: покрытие train'а старыми делителями конечно и коротко. Остаётся сделать решающий шаг от «покрытие мало» к «есть непокрытый центр — и он twin».

В 10. survivor ⇒ twin мы покажем: если в блоке «плохих» центров строго меньше, чем carrier, остаётся выживший, а сито-до-корня превращает его в twin-центр (survivor_of_not_covered, prime_of_no_small_prime_factor); и если такие twin-центры неограничены по \(N\), простых-близнецов бесконечно много (infinite_of_unbounded_centers). Это и есть мост от конечности покрытия — к бесконечности близнецов.

---

← 08. Ограниченный цикл · Оглавление · 10. survivor ⇒ twin →