26. Separating scale: нет ProductHall арифметикой¶

← 25. Rigid-замыкание · Оглавление · 27. Product-core →

В предыдущей главе (25, rigid) мы разобрали локальный fan-in RigidStep X₁ Y, RigidStep X₂ Y и увидели, что коллизия двух legal-подъёмов одного паспорта над общим base упирается в узел uniqueLegalLift: паспорт обязан одновременно различать два фактора (иначе единственность подъёма ложна) и не различать их (иначе конфигурация ProductHall пуста). Эта трилемма — coarse даёт ложность, fine даёт пустоту, tautological даёт циркулярность — осталась открытой.

В настоящей главе мы обходим её честно: не усиливая паспорт, а меняя масштаб. Мы вводим separating scale и показываем, что при нём узел ProductHall на legal-слое закрывается чистой арифметикой, без EPMI, без payment, без steering.

Примечание. Ниже мы аккуратно разделяем два уровня. На уровне логики зон (глава 25) ProductHall разрешался ветвлением uniqueLegalLift/steering, и оба конца были гипотезами. На уровне арифметики масштаба (эта глава) мы вовсе устраняем возможность коллизии: показываем, что при separating scale отображение паспорта уже инъективно на legal-области, поэтому ветка «оба legal, но a₁ ≠ a₂» невозможна как таковая. Это не переименование стены — это её локальное снятие.

Постановка: legal carrier и separating scale¶

Зафиксируем порог A и работаем на legal carrier layer. Активный фактор — это делитель a ∣ N носителя N = 6m + σ, где \(σ ∈ \{-1, +1\}\). Legal-ограничение носителя даёт оценку

\[ 0 < N \le 6X_A + 1, \]

где X_A — верхняя граница центра m на рассматриваемом слое. Наряду с этим у нас есть примориал \(P_A = \prod_{p \le A} p\), задающий coarse-паспорт активного фактора как вычет \(a \bmod P_A\).

Определение 26.1 (separating scale). Мы говорим, что масштаб разделяющий (separating scale), если примориал обгоняет carrier-границу:

\[ 6X_A + 1 < P_A . \tag{26.1} \]

Иначе — центральное определение — это условие, при котором legal-фактор гарантированно меньше модуля паспорта.

Из интуиции: паспорт \(a \bmod P_A\) груб (coarse) как отображение всех натуральных чисел, но на legal-области он видит фактор целиком, если сам фактор не дотягивает до P_A. Именно separating scale и обеспечивает a < P_A, превращая coarse-данные в exact-данные без изменения самого паспорта.

Разделяющая конгруэнция¶

Первый кирпич — элементарная лемма о единственности вычета ниже модуля.

Лемма 26.2 (eq_of_modEq_of_lt). Пусть a₁ < P, a₂ < P и a₁ ≡ a₂ [MOD P]. Тогда a₁ = a₂.

В формулировке Lean:

theorem eq_of_modEq_of_lt {P a₁ a₂ : ℕ} (h1 : a₁ < P) (h2 : a₂ < P)
    (hcong : a₁ ≡ a₂ [MOD P]) : a₁ = a₂

Доказательство исчерпывающе короткое: по определению Nat.ModEq конгруэнция a₁ ≡ a₂ [MOD P] — это равенство остатков a₁ % P = a₂ % P; но при a₁ < P имеем a₁ % P = a₁ (Nat.mod_eq_of_lt), и аналогично для a₂, откуда a₁ = a₂. Содержательно: разность a₁ - a₂ кратна P, но по модулю строго меньше P, значит равна нулю. Это стандартный факт, и мы фиксируем его как самостоятельную лемму, потому что именно он несёт весь арифметический смысл главы — инъективность вычета на области, где представители не достигают модуля.

Граница legal-подъёма¶

Второй кирпич связывает separating scale с положением фактора относительно модуля.

Лемма 26.3 (legal_lift_lt_primorial). Пусть a ∣ N при 0 < a, носитель ограничен N ≤ 6·X_A + 1, 0 < N, и выполнено separating scale 6·X_A + 1 < P_A. Тогда a < P_A.

В формулировке Lean:

theorem legal_lift_lt_primorial {a N X_A P_A : ℕ}
    (hsep : 6 * X_A + 1 < P_A) (hN : N ≤ 6 * X_A + 1) (hdvd : a ∣ N)
    (_hpos : 0 < a) (hNpos : 0 < N) : a < P_A

Доказательство — цепочка неравенств. Из делимости a ∣ N при 0 < N следует a ≤ N (Nat.le_of_dvd); далее a ≤ N ≤ 6X_A + 1 < P_A, откуда a < P_A (в Lean замыкается omega). Заметим, где именно используется каждая гипотеза: делимость даёт a ≤ N, legal-граница носителя даёт N ≤ 6X_A + 1, а separating scale даёт последний строгий шаг 6X_A + 1 < P_A. Убери любую — и вывод a < P_A рушится.

Примечание. Именно здесь separating scale «делает работу». Без него фактор мог бы перевалить за P_A, и тогда \(a \bmod P_A\) уже не восстанавливает a — coarse-паспорт остался бы по-настоящему грубым. Условие P_A > 6X_A + 1 — ровно та точка, в которой grub-паспорт становится exact на legal-области.

Конфигурация ProductHall на legal-слое¶

Абстрактную коллизию, которую мы хотим исключить, удобно упаковать в структуру: два различных legal-фактора над общим base, сравнимых по модулю паспорта и оба ограниченных carrier'ом.

Определение 26.4 (LegalProductHall X_A P_A). Данные: - a₁, a₂ : ℕ — два активных фактора, hne : a₁ ≠ a₂; - hcong : a₁ ≡ a₂ [MOD P_A] — совпадение coarse-паспортов; - носители N₁, N₂ с hdvd₁ : a₁ ∣ N₁, hdvd₂ : a₂ ∣ N₂; - положительность hpos₁ : 0 < a₁, hpos₂ : 0 < a₂; - legal-границы hN₁ : 0 < N₁ ∧ N₁ ≤ 6·X_A + 1 и аналогично hN₂.

Это ровно тот объект, существование которого требовалось в главе 25 для ветки «оба legal, но различны»: одинаковый паспорт (hcong) при различных факторах (hne). Мы утверждаем, что при separating scale такой объект противоречив.

Главная теорема: ProductHall невозможен¶

Теорема 26.5 (no_productHall). При separating scale 6·X_A + 1 < P_A конфигурация LegalProductHall X_A P_A невозможна: из неё выводится False.

В формулировке Lean:

theorem no_productHall {X_A P_A : ℕ} (hsep : 6 * X_A + 1 < P_A)
    (PH : LegalProductHall X_A P_A) : False

Доказательство собирает три предыдущих кирпича. Из Леммы 26.3 (legal_lift_lt_primorial) (применённой к обоим факторам с их carrier-границами) получаем PH.a₁ < P_A и PH.a₂ < P_A. Тогда Лемма 26.2 (eq_of_modEq_of_lt), применённая к PH.hcong, даёт PH.a₁ = PH.a₂. Но это прямо противоречит PH.hne : a₁ ≠ a₂. Формально — PH.hne (eq_of_modEq_of_lt h1 h2 PH.hcong).

Что доказано: при separating scale два legal-фактора, сравнимых по модулю P_A, обязаны совпасть, поэтому пара «различных, но конгруэнтных» не существует. Почему так: separating scale загоняет оба фактора под модуль (< P_A), а под модулем конгруэнтность равносильна равенству.

Вывод. Coarse-паспорт \(a \bmod P_A\) на legal-области инъективен — он различает всё, что вообще там встречается, — и поэтому не может «склеить» два разных фактора. Трилемма из главы 25 обойдена честно: паспорт остался coarse (мы не добавляли ему различающей силы), но на legal-domain он автоматически стал exact.

Примечание (минимальные аксиомы). Формализация no_productHall опирается лишь на propext и Quot.sound и не использует Classical.choice. Это конструктивная арифметика: узел закрыт вычислением, а не выбором. Впервые в программе pump-узел закрыт настоящим доказательством, а не переименованием стены.

Как следствие, коллизия паспортов на legal-слое даёт что угодно по принципу «из ложного — всё» (ex falso, см. словарь):

Следствие 26.6 (productHall_bridge). Для любого утверждения Engine, при separating scale из LegalProductHall X_A P_A следует Engine (через False.elim).

Это не содержательный вывод про двигатель, а честная фиксация: раз конфигурация пуста, мост через неё тривиален. Мы отмечаем это, чтобы не выдавать редукцию за доказательство: productHall_bridge полезен только как логическая заглушка над уже установленной пустотой.

Separating scale достижим — и с огромным запасом¶

Условие P_A > 6X_A + 1 было бы бесполезно, будь оно недостижимо. Наблюдение: примориал растёт экспоненциально по A, тогда как carrier-граница — полиномиально. По теореме Чебышёва

\[ \log P_A = \sum_{p \le A} \log p = \vartheta(A) \sim A, \qquad\text{в десятичной шкале}\quad \log_{10} P_A \sim \frac{A}{\ln 10}. \]

Если положить самую пессимистичную оценку носителя вида \(6X_A + 1 \lesssim 6\,A^{4.5}\), то её логарифм \(\log_{10}(6A^{4.5}) \approx 4.5\log_{10}A + \log_{10}6\) растёт лишь как A^{4.5} в логарифмической шкале, тогда как \(\log_{10}P_A\) растёт линейно по A. Линейное \(A/\ln 10\) обгоняет \(4.5\log_{10}A\) уже при A ≈ 50, и дальше разрыв только ширится:

`A`	\(\log_{10} P_A\)	\(\log_{10}(6\,A^{4.5})\)	`P_A > 6X_A + 1`
50	17.0	8.4	✓
200	81.1	11.1	✓
1000	414.5	14.3	✓

Разрыв к A = 200 — семьдесят порядков (81 против 11).

Итог раздела. Separating scale не только достижим, но выполняется с колоссальным запасом: экспонента примориала мгновенно перекрывает любую полиномиальную carrier-границу. Условие реалистично, и на нём можно строить.

Куда переехала трудность (честно)¶

Закрытие ProductHall не закрывает всю программу — оно сужает её. Энергодефектная трихотомия имела вид LowerRankCollision ∨ ProductHall; сняв правую ветвь, мы схлопываем её в одну:

Лемма 26.7 (trichotomy_collapses). (L ∨ PH) ∧ ¬PH ⟹ L.

Это чистая логика (Or.resolve_right), и она честно оформлена как редукция, а не как результат: сам предикат energy_defect_trichotomy, порождающий дизъюнкцию L ∨ PH, остаётся открытым узлом. Точно так же мы фиксируем скелет спуска по рангу:

Лемма-скелет 26.8 (rank_descent_terminates). При наличии редукции ранга r → r-1 на диапазоне 1 < r ≤ 4 и закрытия ранга 1 (SNOL) спуск \(r → \dots → 1\) конечен.

Здесь lower_step (реальная редукция ранга) и rank1_closes (закрытие rank-1 через SNOL) — явные гипотезы, а не теоремы. Мы не выдаём каркас за доказательство: он лишь показывает, что если содержательные шаги предъявлены, well-founded индукция по r ≤ 4 их собирает.

Гипотеза и план закрытия. Дыра не исчезла — она переехала на rank-уровень и стала точнее. Открытыми остаются: (1) energy_defect_trichotomy — что коллизия product-подписи с mismatch даёт LowerRankCollision ∨ ProductHall; (2) закрытие rank-1 через SNOL; (3) ограниченная rank-индукция r ≤ 4. План: глобальный pigeonhole (бесконечно много родословных при конечном ключе — пижонхол, см. словарь) должен давать LowerRankCollision на каждом ранге — тот же fan-in аргумент, но на ранг ниже, — а separating scale, доказанный здесь, обеспечивает инъективность паспорта на верхнем legal-слое как базу этого спуска. Ключевое напряжение, которое предстоит разрешить: паспорт должен быть fine для леммы единственности и coarse для pigeonhole одновременно — та же трилемма, поднятая на ранг выше.

Итог и мост к следующей главе¶

Мы ввели separating scale P_A > 6X_A + 1, показали его достижимость с экспоненциальным запасом и на трёх арифметических леммах (eq_of_modEq_of_lt, legal_lift_lt_primorial, no_productHall) закрыли узел ProductHall на legal-слое конструктивно, без Classical.choice. Трилемма uniqueLegalLift обойдена не усилением паспорта, а сжатием факторов под модуль: на legal-области coarse-паспорт \(a \bmod P_A\) инъективен, и потому «различные, но конгруэнтные» факторы невозможны.

Однако вся эта арифметика работала с плоским фактором a ∣ N. Чтобы перенести инъективность на весь спуск по рангу, недостаточно одного числа — нужна экстенсиональная модель состояния, различающая роли факторов и не тянущая за собой many-to-one хвост абсорбера.

В следующей главе (27, product-core) мы вводим RankNode r — конкретное product-ядро factors : Fin r → ℕ со знаком, — и переносим no_productHall с плоского фактора на это ядро: покажем, что при факторах < P_A совпадение core-подписи влечёт покомпонентное равенство. Это превращает арифметику одной главы в экстенсиональность, на которой можно строить rank-descent.

← 25. Rigid-замыкание · Оглавление · 27. Product-core →