Носитель двойки: shared gcd делит 2¶
← 01. Двигатель (EPMI) · Оглавление · 03. Сохранение двойки →
В предыдущей главе 01. Двигатель (EPMI) мы построили центральный объект программы — вечный двигатель Евклида — и установили, что его локальная невозможность держится на строго убывающем ресурсе высоты. Прежде чем спускаться по цепи звеньев, нам нужно понять, что именно в паре близнецов остаётся неизменным при спуске и что разделяет её стороны. Настоящая глава выделяет этот инвариант в чистом, элементарно проверяемом виде: разность сторон равна двойке, и вся арифметика взаимодействия сторон с простыми делителями подчинена этому числу.
Постановка¶
Мы работаем с центрами близнецовых пар. Каждой паре простых-близнецов отвечает целое \(m \ge 1\), при котором обе стороны
представляют кандидатов на простоту. Форма \(6m \pm 1\) не случайна: всякое простое \(p > 3\) лежит в одном из классов вычетов \(\pm 1 \pmod 6\), поэтому близнецовая пара с разностью \(2\), оба члена которой больше \(3\), неизбежно центрируется в кратном шести. Число \(m\) мы называем центром, а выражения \(6m-1\), \(6m+1\) — сторонами центра.
Примечание. Условие \(m \ge 1\) здесь несёт двойную нагрузку. Во-первых, оно исключает вырожденный случай \(m=0\), при котором «сторона» \(6m-1\) обращается в \(-1\) и в натуральной арифметике теряет смысл. Во-вторых — и это существеннее для формализации — при работе в \(\mathbb{N}\) вычитание усечённое (\(6m-1\) при \(m=0\) дало бы \(0\), а не \(-1\)), так что предпосылка \(1 \le m\) гарантирует, что \(6m-1\) есть честный предшественник \(6m\), и тождество \(6m+1 = (6m-1)+2\) выполняется как равенство натуральных чисел.
Вопрос главы предельно конкретен: как общий делитель двух сторон соотносится с их разностью, и что это влечёт для простых, «сидящих» одновременно на обеих сторонах?
Двойка как разность сторон¶
Начнём с наблюдения, из которого вырастает всё остальное. Стороны отстоят друг от друга ровно на \(2\):
Естественно предположить, что именно эта фиксированная разность управляет всей совместной делимостью сторон. Формализуем это.
Определение 2.1 (общий делитель сторон). Простое (или, в общей формулировке, любое натуральное) \(p\) называется общим делителем сторон центра \(m\), если одновременно
Первая теорема главы утверждает, что всякий такой \(p\) вынужден делить двойку.
Теорема 2.2 (
twin_sides_shared_dvd_two). Пусть \(m \ge 1\), и пусть \(p \mid (6m+1)\) и \(p \mid (6m-1)\). Тогда \(p \mid 2\).
Смысл утверждения: общий делитель сторон не может быть больше, чем позволяет их разность. Доказательство прозрачно и опирается на одно тождество и одно свойство делимости.
Разбор доказательства. Ключевой шаг — переписать бо́льшую сторону через меньшую:
В Lean это равенство закрывается тактикой omega (линейная арифметика над \(\mathbb{N}\) с учётом усечённого вычитания при \(m \ge 1\)). После подстановки гипотеза \(p \mid (6m+1)\) превращается в
Теперь применяется базовое свойство делимости: если \(p\) делит сумму и делит одно из слагаемых, то делит и второе. В ядре Lean 4 это Nat.dvd_add_right: из \(p \mid (6m-1)\) следует эквивалентность \(p \mid \big((6m-1)+2\big) \iff p \mid 2\), и левая часть у нас в руках. Отсюда \(p \mid 2\). \(\qquad\blacksquare\)
Примечание. Ни одно из чисел \(6m\pm1\) в это доказательство по существу не входит — работает только их разность. То же рассуждение дало бы: любой общий делитель двух чисел делит их разность, а значит \(\gcd(6m-1, 6m+1) \mid 2\). Формулировка через \(p \mid 2\) выбрана потому, что в дальнейшем нас интересует именно поведение простых делителей, а не численное значение \(\gcd\); но содержательно теорема — это в точности утверждение \(\gcd(6m-1,\,6m+1) \mid 2\).
Эксклюзивность: большой простой делит не более одной стороны¶
Из делимости двойки немедленно вытекает содержательное следствие. Двойка мала: её единственные натуральные делители суть \(1\) и \(2\). Поэтому если общий делитель сторон вообще нетривиален, он равен \(2\); а любой простой \(p > 2\) общим делителем быть не может.
Теорема 2.3 (
no_large_shared_divisor). Пусть \(m \ge 1\) и \(p > 2\). Тогда невозможно одновременно \(p \mid (6m+1)\) и \(p \mid (6m-1)\).
Иными словами (это и есть эксклюзивность): простой \(p > 2\) делит не более одной из двух сторон. Он вправе делить \(6m-1\), вправе делить \(6m+1\), но не обе сразу — обе занял бы только делитель двойки, а \(p>2\) таковым не является.
Разбор доказательства. Рассуждение — короткая цепочка от предыдущей теоремы к противоречию. Из предположения, что \(p\) делит обе стороны, Теорема 2.2 (twin_sides_shared_dvd_two) даёт \(p \mid 2\). Далее используется: делитель положительного числа не превосходит его, — в Lean это Nat.le_of_dvd (положительность \(2 > 0\) проверяется decide), откуда \(p \le 2\). Но по условию \(2 < p\). Неравенства \(p \le 2\) и \(2 < p\) несовместны; противоречие закрывается тактикой omega. \(\qquad\blacksquare\)
Примечание. Обе теоремы файла
Engine/Carrier.leanдоказаны в чистом ядре Lean 4 — безmathlib, на трёх примитивах: тождество (omega), перенос слагаемого (Nat.dvd_add_right) и оценка делителя (Nat.le_of_dvd). Это делает результат частью строго проверенного, самодостаточного фундамента программы: здесь нет ни редукции к недоказанному, ни скрытой гипотезы — только элементарная делимость.
Что это значит для программы: двойка как носитель¶
Теперь соберём смысл. У пары близнецов есть единственный делитель, разделяемый обеими сторонами, — и это двойка (когда она вообще есть; для нечётных сторон общий делитель тривиален, \(\gcd = 1\)). Все нетривиальные простые делители сторон эксклюзивны: каждый принадлежит ровно одной стороне. Именно это разделение простых на два непересекающихся (по большим простым) множества и есть структурный факт, который мы будем эксплуатировать при спуске.
В терминологии Lean-комментария это «shared active gcd \(= 0\)»: ни один активный простой \(p > A \ge 2\) не делит обе стороны, так что shared-active класс пуст. Двойка изъята из активного слоя как заведомо малый простой, и на активном уровне стороны делимостно независимы. Это ровно та независимость, которая нужна детерминантному закону rank-\((3,3)\) 05. Необратимость: раскладывая \(6m-1 = abv\) и \(6m+1 = qrs\) в произведения активных простых, мы вправе считать все шесть множителей \(a,b,v,q,r,s\) различными — эксклюзивность запрещает совпадение делителя между сторонами.
Отсюда и метафора носителя. Двойка — это то, что через всю программу разделяет стороны (гарантируя эксклюзивность больших простых) и одновременно переносится при спуске: при удалении активного множителя descended-центр наследует ту же разность \(2\) между своими сторонами. Спуск меняет масштаб центра, перекраивает разложения, но не трогает величину, отделяющую \(6m'-1\) от \(6m'+1\). Двойка инвариантна к спуску — она и есть его несущий каркас.
Наблюдение. Полезно видеть в этом дискретный аналог «сохраняющейся величины». Высота \(H\) из главы 01. Двигатель (EPMI) строго убывает и тем самым запрещает вечное движение; разность \(2\), напротив, строго сохраняется и тем самым фиксирует геометрию каждого звена. Убывающий ресурс и сохраняющийся носитель — две стороны одного механизма: первый гонит спуск к дну, второй следит, чтобы на каждом шаге объект оставался близнецовой парой с той же щелью.
Мост к следующей главе¶
Мы установили, что двойка разделяет стороны и что большие простые эксклюзивны. Осталось проверить утверждение, которое здесь прозвучало лишь как обещание: что разность \(2\) действительно переживает операцию спуска, а не восстанавливается по совпадению на каждом шаге. В следующей главе 03. Сохранение двойки мы формализуем сохранение двойки при descend'е — покажем, что после удаления активного множителя новая пара сторон снова отстоит ровно на \(2\), — и тем самым превратим носитель из наблюдения в инвариант, на который можно опереться в бесконечном спуске.
← 01. Двигатель (EPMI) · Оглавление · 03. Сохранение двойки →