Перейти к содержанию

28. Факторизация: RankNode из составной стороны

← 27. Product-core · Оглавление · 29. Последнее звено →

Lean-источник: Engine/MkNode.lean (пространство имён EuclidsPath.MkNode, open EuclidsPath.ProductCore). Вся арифметика этой главы доказана без аксиом и без sorry.

В предыдущей главе о product-core мы зафиксировали конечную сцену двигателя: узел ранга r как экстенсиональный объект RankNode r, состоящий из знака sign и роль-индексированного семейства факторов factors : Fin r → ℕ, вместе с сертификатом AmbientLegal, гарантирующим, что все факторы делят один top-side N₀ ≤ 6X_A+1. Но сцена оставалась пустой: мы описали, каким должен быть узел, и доказали, что на таких узлах невозможен ProductHall, — однако не предъявили ни одного узла.

Настоящая глава заполняет этот пробел. Мы покажем, как из чистой арифметики составной стороны центра m построить конкретный RankNode r с 2 ≤ r ≤ 4, факторами > A и сертификатом AmbientLegal. Это тот кирпич, из которого следующая глава соберёт бесконечный поток узлов.

28.1. Постановка: от центра к разложению

Напомним геометрию несущего пространства. Каждый кандидат в twin-центры — это число m, а его две стороны суть

\[ 6m - 1 \quad\text{и}\quad 6m + 1 . \]

Центр является twin-центром ровно тогда, когда обе стороны просты. Если хотя бы одна сторона составна, центр «промахивается», и именно этот промах мы хотим превратить в структуру. Составная сторона N раскладывается в произведение простых, и это разложение — не что иное, как список факторов будущего RankNode. Задача главы: доказать, что этот список имеет длину между 2 и 4, что все его элементы превосходят A, и что он несёт сертификат AmbientLegal.

Примечание. Параметр A — это верхняя граница «малых» простых, отфильтрованных ситом. Условие Clean A m (см. §28.5) означает, что ни одно простое q ≤ A не делит ни одну из сторон центра m. Именно чистота центра заставляет все простые факторы составной стороны быть большими, > A, — а это, в свою очередь, ограничивает число факторов сверху.

28.2. Нижняя оценка произведения: (A+1)^len ≤ prod

Первый и самый элементарный факт — оценка снизу на произведение списка факторов через его длину.

Определение 28.1 (список больших факторов). Пусть L : List ℕ — список натуральных чисел. Скажем, что L состоит из факторов, больших A, если

\[ \forall a \in L,\quad A < a . \]

Теорема 28.2 (prod_ge_of_factors_gt). Если каждый элемент списка L строго больше A, то

\[ (A+1)^{\lvert L\rvert} \le \prod L , \tag{28.1} \]

где |L| — длина списка, а ∏ L = L.prod — произведение его элементов.

Что доказано и почему. Доказательство идёт индукцией по списку. Для пустого списка обе части равны 1 ((A+1)^0 = 1 = ∏ []). На шаге cons x xs мы используем, что каждый элемент, будучи > A, удовлетворяет A + 1 ≤ x (в натуральных числах строгое неравенство A < x эквивалентно A + 1 ≤ x), а по индукционному предположению (A+1)^{|xs|} ≤ ∏ xs. Перемножая эти два неравенства монотонностью умножения (Nat.mul_le_mul), получаем

\[ (A+1)^{|xs|}\cdot(A+1) \;\le\; \bigl(\textstyle\prod xs\bigr)\cdot x , \]

а левая часть есть в точности (A+1)^{|xs|+1} = (A+1)^{|L|}, правая же после перестановки множителей (ring) равна ∏ L. Здесь важна замена x * ∏ xs = (∏ xs) * x, чтобы согласовать порядок с List.prod_cons.

Что это значит. Оценка переводит утверждение о количестве факторов в утверждение о величине произведения. Каждый фактор весит не меньше A+1, поэтому длинный список из больших факторов даёт экспоненциально большое произведение. Именно это позволит нам ограничить длину сверху, зная, что произведение не может быть слишком большим.

28.3. Ранг не превосходит четырёх: factor_rank_le_four

Теперь мы соединяем нижнюю оценку §28.2 с масштабным ограничением. Ключевое наблюдение: составная сторона N легального центра не превосходит 6X_A + 1, а сито настроено так, что этот порог сам меньше A^5. Из интуиции разложения ясно, что «слишком много» больших факторов не помещается под таким потолком.

Теорема 28.3 (factor_rank_le_four). Пусть 1 ≤ A, список L состоит из факторов > A, его произведение удовлетворяет ∏ L ≤ 6X_A + 1, и выполнено масштабное неравенство 6X_A + 1 < A^5. Тогда

\[ \lvert L\rvert \le 4 . \]

Что доказано и почему. Рассуждаем от противного. Предположим |L| ≥ 5 (в Lean это записано как 4 < |L| после not_le). Тогда, комбинируя монотонность степени по показателю (Nat.pow_le_pow_right) с нижней оценкой Теоремы 28.2 (prod_ge_of_factors_gt), получаем цепочку

\[ (A+1)^5 \;\le\; (A+1)^{\lvert L\rvert} \;\le\; \prod L \;\le\; 6X_A + 1 \;<\; A^5 . \tag{28.2} \]

С другой стороны, поскольку A ≥ 1, строго возрастает основание степени:

\[ A^5 \;<\; (A+1)^5 \]

(лемма Nat.pow_lt_pow_left с A < A+1). Итого мы имеем одновременно (A+1)^5 ≤ 6X_A+1 < A^5 и A^5 < (A+1)^5, что даёт (A+1)^5 < (A+1)^5 — противоречие, закрываемое omega.

Что это значит. Это и есть источник магического числа 4 во всей конструкции двигателя. Ранг узла — число простых факторов составной стороны — ограничен сверху четвёркой не по определению и не по соглашению, а как арифметическое следствие масштаба сита 6X_A + 1 < A^5. Пять больших факторов дали бы произведение не меньше (A+1)^5 > A^5, что не влезает под потолок 6X_A + 1.

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

Примечание. Масштабное неравенство 6X_A + 1 < A^5 — не гипотеза, а проверяемое свойство настройки сита; здесь оно входит как явная гипотеза hscale, чтобы теорема оставалась чистой арифметикой без привязки к конкретному X_A. Показатель 5 — это 4 + 1: он ровно на единицу больше искомой границы ранга, что и делает шаг «пять факторов ⟹ произведение ≥ (A+1)^5 > A^5» решающим.

28.4. Ранг не меньше двух: composite_rank_ge_two

Верхняя граница ранга бесполезна без нижней: узел ранга 0 или 1 не был бы разложением составного числа. Нижнюю границу даёт само определение составности.

Теорема 28.4 (composite_rank_ge_two). Если 1 < N и N не простое (¬ N.Prime), то список простых множителей имеет длину не меньше двух:

\[ 2 \le \bigl\lvert \mathrm{primeFactorsList} N\bigr\rvert . \]

Что доказано и почему. Отправная точка — тождество Nat.prod_primeFactorsList: для N ≠ 0 произведение канонического списка простых множителей равно самому N. Далее — разбор от противного по длине списка (interval_cases при |L| < 2):

  • Длина 0 означала бы L = [], откуда ∏ L = 1, то есть N = 1, что противоречит 1 < N.
  • Длина 1 означала бы L = [p] с единственным простым p (по List.length_eq_one_iff). Тогда ∏ L = p = N, а поскольку p — простое (по Nat.prime_of_mem_primeFactorsList), само N оказалось бы простым, что противоречит ¬ N.Prime.

Оба случая ведут к противоречию, значит длина не меньше 2.

Что это значит. Составность — это ровно наличие как минимум двух простых множителей (с учётом кратности). Формально этот тривиальный на бумаге факт требует аккуратного связывания трёх лемм mathlib о primeFactorsList, и здесь он доказан начисто. Вместе с §28.3 получаем зажатую вилку \(2 \le r \le 4\) — конечный диапазон рангов узла.

28.5. Чистый центр заставляет факторы быть большими: prime_factor_gt_A_*

Осталось объяснить, откуда берётся условие «все факторы > A», которое мы всюду использовали как гипотезу. Оно вытекает из чистоты центра.

Определение 28.5 (Clean A m). Центр m чист относительно A, если ни одно простое q ≤ A не делит ни одну из его сторон:

\[ \forall q\ \text{prime},\ q \le A \;\Rightarrow\; \neg\bigl(q \mid (6m-1)\ \lor\ q \mid (6m+1)\bigr). \]

Теорема 28.6 (prime_factor_gt_A_plus, prime_factor_gt_A_minus). Пусть центр m чист (Clean A m), p — простое. Если p ∣ (6m + 1) (соответственно p ∣ (6m - 1)), то

\[ A < p . \]

Что доказано и почему. Доказательство обеих версий — прямое противопоставление. Предположим p ≤ A. Тогда p — простое, не превосходящее A, делящее одну из сторон, что в точности отрицает условие чистоты Clean A m (в случае plus — через Or.inr hdvd, в случае minus — через Or.inl hdvd). Противоречие; значит A < p.

Что это значит. Это лемма-мост между ситом и разложением. Сито гарантирует, что у выживших центров нет мелких простых делителей на сторонах; следовательно, любой простой множитель составной стороны автоматически велик, > A. Именно это свойство подаёт гипотезу hgt во все предыдущие теоремы — и замыкает вилку 2 ≤ r ≤ 4 на конкретном разложении конкретной стороны.

28.6. Выбор составной стороны: composite_side_of_not_twin

Прежде чем строить узел, надо выбрать, какую сторону раскладывать. У промахнувшегося центра составна хотя бы одна из двух сторон — и её мы возьмём.

Теорема 28.7 (composite_side_of_not_twin). Пусть обе стороны нетривиальны, 1 < 6m - 1 и 1 < 6m + 1, и центр не twin, то есть неверно, что обе стороны просты (¬ ((6m-1).Prime ∧ (6m+1).Prime)). Тогда существует составная нетривиальная сторона:

\[ \bigl(1 < 6m-1\ \land\ \neg(6m-1)\ \text{prime}\bigr)\ \lor\ \bigl(1 < 6m+1\ \land\ \neg(6m+1)\ \text{prime}\bigr). \]

Что доказано и почему. Разбор по случаям простоты нижней стороны. Если 6m - 1 не простое — берём его (левый дизъюнкт). Если же 6m - 1 простое, то из отрицания twin-условия следует, что 6m + 1 не может быть простым, и мы берём верхнюю сторону (правый дизъюнкт). Случай, когда обе стороны простые, невозможен — он прямо противоречит ¬ (…∧…) через absurd.

Что это значит. Отрицание twin-центра — чисто логическое утверждение «не обе просты» — конструктивно превращается в предъявление конкретной составной стороны. Это переход от «центр промахнулся» к «вот число, которое мы разложим». Требование 1 < сторона отсекает вырожденные малые центры, где сторона равна 1 и разложения нет.

28.7. Сборка узла: mkNode_of_composite

Все ингредиенты готовы. Составная сторона N даёт список простых множителей; §28.4 гарантирует длину ≥ 2, §28.3 — длину ≤ 4, §28.5 — что все множители > A. Осталось упаковать это в RankNode с сертификатом AmbientLegal.

Определение 28.8 (AmbientLegal, напоминание из главы 27). Семейство factors : Fin r → ℕ легально в окружении X_A, если найдётся общий top-side N₀, который они все делят и который не превосходит потолка сита:

\[ \exists N_0,\ 0 < N_0\ \land\ N_0 \le 6X_A + 1\ \land\ \forall i,\ \mathtt{factors}\,i \mid N_0 . \]

Теорема 28.9 (mkNode_of_composite). Пусть 1 ≤ A, 1 < N, число N составно, оно не превосходит потолка N ≤ 6X_A + 1, выполнено масштабное неравенство 6X_A + 1 < A^5, и каждый простой делитель N больше A (∀ p, p.Prime → p ∣ N → A < p). Тогда для любого знака sgn : Sign существует ранг r с 2 ≤ r ≤ 4 и узел X : RankNode r такой, что

\[ \mathtt{AmbientLegal}\ X_A\ X.\mathtt{factors}\qquad\text{и}\qquad \prod \bigl(\mathrm{ofFn} X.\mathtt{factors}\bigr) = N . \tag{28.3} \]

Что доказано и почему. Строим узел явно. Пусть L = primeFactorsList N. Тогда:

  • hr2 : 2 ≤ |L| — из Теоремы 28.4 (composite_rank_ge_two, §28.4);
  • hgt : ∀ a ∈ L, A < a — каждый элемент списка есть простой делитель N (Nat.prime_of_mem_primeFactorsList, Nat.dvd_of_mem_primeFactorsList), а гипотеза hbig делает его > A (это §28.5, поданное как вход);
  • hprodN : ∏ L = N — тождество Nat.prod_primeFactorsList;
  • hr4 : |L| ≤ 4 — из Теоремы 28.3 (factor_rank_le_four, §28.3), где посылка ∏ L ≤ 6X_A+1 получается подстановкой ∏ L = N ≤ 6X_A+1.

В качестве ранга берём r = |L|, а сам узел — ⟨sgn, fun i => L.get i⟩: знак фиксируется извне, факторы — это элементы списка, индексированные Fin |L|. Остаётся проверить два обязательства:

  1. AmbientLegal: берём свидетель — конкретный объект, удостоверяющий утверждение (см. словарь), — N₀ = N. Он положителен (из 1 < N), не превосходит потолка (hNle), и каждый L.get i делит N, поскольку делит произведение ∏ L = N (List.dvd_prod для элемента списка List.get_mem).
  2. Согласование произведения: (ofFn (L.get ·)).prod = ∏ L по List.ofFn_get (восстановление списка из своих компонент), а ∏ L = N уже установлено.

Что это значит. Это центральная теорема главы — «Theorem 7.1» в нумерации источника. Она превращает арифметический факт (составная сторона имеет 2..4 больших простых множителя) в структурный объект сцены двигателя: настоящий RankNode с сертификатом легальности. Знак sgn подаётся снаружи, потому что он кодирует, какая из двух сторон была составной, — эта информация приходит из §28.6, а не из самого разложения.

Важно подчеркнуть: узел строится конструктивно, а не постулируется; произведение его факторов доказуемо равно исходной стороне N, то есть узел — точное разложение, а не абстрактный ярлык.

Примечание (никакой редукции за доказательство). Все семь утверждений этой главы — prod_ge_of_factors_gt, factor_rank_le_four, composite_rank_ge_two, prime_factor_gt_A_plus, prime_factor_gt_A_minus, composite_side_of_not_twin, mkNode_of_composite — доказаны полностью, без sorry и без аксиом сверх mathlib. Это чистая арифметика факторизации: она не предполагает никакого свойства двигателя и ничего о нём не утверждает. Здесь нет открытых узлов.

28.8. Где проходит граница доказанного и мост к главе 29

Стоит явно очертить, что эта глава не делает, чтобы не выдать частичный результат за целое. Мы показали: данный чистый центр m, промахнувшийся мимо twin, поставляет один легальный RankNode ранга 2..4. Мы не показали здесь, что таких центров бесконечно много и что среди них бесконечно много одного и того же ранга. Именно это — единственный содержательный вход (гейт: честно названное недостающее утверждение, см. словарь), отделяющий локальную факторизацию от глобального запуска двигателя.

Гипотеза, выносимая в следующую главу. Существует бесконечное множество чистых центров (это уже доказанный факт Residuals.carrier_nonempty_above: над любым N найдётся clean-центр), и, применяя mkNode_of_composite к каждому, мы получаем бесконечное семейство узлов. По pigeonhole на конечном множестве рангов {2,3,4} бесконечно много узлов имеют один ранг r. План закрытия: оформить это как структуру FactorizationData — бесконечное подмножество центров фиксированного ранга с инъективной, AmbientLegal-сертифицированной картой node : ℕ → RankNode r.

Иными словами, mkNode_of_composite — это «фабрика узлов», а следующая глава подключает к ней бесконечный конвейер: carrier bridge возьмёт доказанную бесконечность чистых центров, прогонит её через факторизацию этой главы, применит infinite-pigeonhole по рангу и предъявит тот самый FactorizationData, из которого product-core собирает Engine. К этому мосту — от единичного узла к бесконечному потоку узлов одного ранга — мы и переходим.

← 27. Product-core · Оглавление · 29. Последнее звено →