17. Закон оплаты и дефект¶

← 16. От противного · Оглавление · 18. SNOL →

Lean-источник: Engine/PaymentLedger.lean (5 теорем, стандартные аксиомы, без sorry). Числовой стресс-тест: tools/RESULTS_payment_budget.md.

Где мы находимся¶

В главе 16 мы свели всю программу к единственной типизированной гипотезе H и показали, что она дословно упирается в стену чётности: условная теорема twin_finite_contradiction («конечность близнецов вместе с H влечёт False») собрана и машинно проверена, но само H — строгий реальный four-corner плюс нижняя оценка carrier — не выводится distribution-free из имеющихся идей.

Естественно спросить: нет ли у остановки двигателя алгебраической цены, которую можно предъявить без распределения? В этой главе мы вводим такую цену — закон оплаты — и доказываем её ядро элементарно (только Nat/Int и Finset, без анализа и сита). Одновременно мы честно локализуем, где этот маршрут вновь встречает ту же стену.

Ведущая интуиция такова: когда двигатель Евклида останавливается — он платит, и оплата подчинена строгому порядку. Boundary-смерть S → ⊥ не бесплатна; каждый бесплатный проход к упорядоченному простому p обязан внести делимостной charge, а если такого charge нет — платится compatibility tax. Оплата распределена по малым простым, и у каждого из них есть конечная ёмкость. Ниже мы делаем эту картину точной.

Канальный закон: ровно `p − 2` совместимых канала¶

Зафиксируем геометрию. Центры кандидатов в близнецы лежат в классе 6ℤ, а стороны имеют вид 6n ± 1; знаки мы обозначаем через ε, σ ∈ {+1, −1}. Подъём источника m к активному простому a через границу с параметром n описывается линейным соотношением

\[ 6m + \sigma \;=\; a\,(6n + \varepsilon). \]

Пусть простое p > 3 ловит противоположную сторону границы, то есть p ∣ 6n − ε. Спрашивается: в каком классе вычетов по модулю p вынужден лежать источник m?

Определение 17.1 (канальный класс). При заданных a, ε, σ и простом p источник m называется совместимым каналом по p, если выполнено соотношение подъёма и граничное условие p ∣ 6n − ε. Каналом мы называем допустимый класс вычетов $6m \bmod p$.

Теорема 17.2 (channel_residue). Если p > 3, 6m + σ = a(6n + ε) и p ∣ 6n − ε, то

\[ 6m \;\equiv\; 2a\varepsilon - \sigma \pmod p. \]

Доказательство — чистая CRT-алгебра. Из 6n ≡ ε (mod p) получаем 6n + ε ≡ 2ε, откуда a(6n + ε) ≡ 2aε; подставляя 6m + σ = a(6n + ε), имеем 6m + σ ≡ 2aε, то есть 6m ≡ 2aε − σ. В Lean это ровно две тождественные перестановки колец: сначала a(6n + ε) − 2aε = a(6n − ε) (делится на p по граничному условию), затем 6m − (2aε − σ) = a(6n + ε) − 2aε.

Что это значит. Класс 6m не свободен — он прибит к одному вычету по p. Значит из полного набора вычетов чистый источник может занять не все, а лишь совместимые. Сама сторона и класс 0 (тривиальная делимость на p) исключены, и подсчёт совместимых каналов даёт ровно p − 2 штук — в точности столько же, сколько несёт carrier (ср. §13.1). Иными словами, малое простое p не создаёт грубого дефицита ёмкости: у него p − 2 канала, и одиночного переполнения одного p нет.

Примечание. Это первый честный урок главы: наивная надежда «ёмкость одного простого переполнится и сломает структуру» численно не подтверждается. p каналов ровно столько, сколько нужно. Рычаг придётся искать не в одном p, а в совместности по всем малым q сразу.

Закон налога: θ-дихотомия¶

Перейдём к противоположной стороне 6m − σ. На ней малое простое q может наложить дополнительный запрет — новый исключённый класс, — и это стоит ёмкости. Ключевое наблюдение: этот дополнительный запрет иногда исчезает, а именно когда он совпадает с уже запрещённым классом.

Определение 17.3 (сдвиг θ). Полагаем θ := σε. Проход по q называется безналоговым, если дополнительный запрет по q на стороне 6m − σ совпадает с ранее исключённым классом, то есть не отнимает новой ёмкости.

Теорема 17.4 (no_tax_iff_shifted). Безналоговость по q равносильна делимости сдвига:

\[ q \mid a - \theta \quad\Longleftrightarrow\quad a \equiv \theta \pmod q. \]

Формально в Lean это тождество Int.modEq_iff_dvd вместе с dvd_sub_comm: q ∣ a − θ есть в точности a ≡ θ [ZMOD q]. Содержательно же дихотомия читается так:

\[ \text{налог по } q \;=\; \begin{cases} 0, & q \mid a - \theta \quad(\text{совместимо, сдвиг делится}),\\[4pt] \dfrac{q-3}{q-2}, & q \nmid a - \theta \quad(\text{новый запрет, ёмкость падает}). \end{cases} \tag{17.1} \]

Фактор (q-3)/(q-2) — это доля выживающей ёмкости после того, как из q − 2 совместимых каналов дополнительный запрет вычеркивает ещё один. Так закон оплаты получает точную цену: за каждое малое простое q, по которому активное a не согласовано со сдвигом θ, двигатель платит фактором (q-3)/(q-2).

Примечание. Дихотомия детерминирована и алгебраична: никакого распределения здесь ещё нет. «Бесплатно» — только когда q ∣ a − θ; во всех прочих случаях — фиксированный налог. Это и есть формальная запись тезиса «оплата не бесплатна» на уровне одного простого.

Примориал делит сдвиг¶

Соберём безналоговые простые вместе. Пусть G — множество малых простых, по каждому из которых проход безналоговый. Тогда все делимости q ∣ a − θ складываются, и — поскольку различные простые попарно взаимно просты — их произведение тоже делит сдвиг.

Определение 17.5 (примориал по G). Для конечного множества попарно взаимно простых q обозначим $P := \prod_{q \in G} q$. Это примориал (произведение) малых простых, по которым проход безналоговый.

Теорема 17.6 (primorial_dvd_shift). Если (G).Pairwise Nat.Coprime и ∀ q ∈ G, q ∣ a − θ, то

\[ \Bigl(\prod_{q \in G} q\Bigr) \;\Bigm|\; a - \theta. \]

Доказательство — Finset.prod_dvd_of_coprime: произведение попарно взаимно простых делителей общего аргумента делит этот аргумент (делимости складываются как lcm, а для взаимно простых lcm совпадает с произведением). Взаимную простоту q над ℤ мы переносим из Nat.Coprime через isCoprime.intCast.

Почему это важно. Индивидуальные налоги были дешёвыми и локальными; но их отсутствие сразу по многим q — не бесплатно, оно накладывает глобальное делимостное условие на сдвиг: весь примориал безналоговых простых обязан делить a − θ. Совместность по всем q < p — вот настоящий рычаг, а не ёмкость одного простого.

Закон дефекта¶

Теперь примориал вступает в конфликт с размером активного простого. Делитель не может превосходить ненулевую делимую величину — отсюда жёсткая нижняя оценка на разность.

Теорема 17.7 (shifted_primorial_bound). Если P ∣ a − θ и a ≠ θ, то

\[ P \;\le\; |a - \theta|. \]

Доказательство: из a ≠ θ следует a − θ ≠ 0, значит |a − θ| > 0; тогда Int.le_of_dvd вместе с dvd_abs даёт P ≤ |a − θ|. Это и есть закон дефекта в точной форме.

Смысл прямой и сильный. Бесплатный проход к упорядоченному простому p требует безналоговости по всем меньшим малым простым, а значит — что a − θ делится на весь примориал P_{<p} малых простых до p. Но тогда либо a = θ (тривиальный, вырожденный случай), либо примориал ограничен активным делителем: $P_{<p} \le |a - θ|$.

Вывод. Как только примориал перерастает активный делитель, нетривиального безналогового прохода просто нет.

Определение 17.8 (порог Y_A). Пусть Z — верхняя граница активного делителя на масштабе A (|a − θ| ≤ Z). Порогом Y_A называется наименьшее простое p, для которого примориал малых простых до p превосходит Z, то есть P_{<p} > Z. Для p ≥ Y_A бесплатный проход требует a = θ.

Теорема 17.9 (late_boundary_not_free). Если P ∣ a − θ, |a − θ| ≤ Z и Z < P, то a = θ.

Это контрапозиция закона дефекта: предположив a ≠ θ, из Теоремы 17.7 (shifted_primorial_bound) получаем P ≤ |a − θ| ≤ Z < P — противоречие (в Lean замыкается omega). Значит поздняя граница не бесплатна: за порогом Y_A не существует нетривиального a ≤ Z, делящегося на примориал, а потому безналоговый (бесплатный) проход к позднему p невозможен.

Примечание. Численно (tools/RESULTS_payment_budget.md и сопутствующий аудит) порог наступает рано: $Y_A / A ≈ 0.15\text{–}0.6$, и эта доля падает с ростом масштаба. То есть бесплатных поздних границ почти нет — примориал малых простых обгоняет активный делитель, и закон дефекта кусается для подавляющего большинства поздних p.

Где ёмкость переполняется — и где стена¶

Собранное ядро — пять доказанных теорем — даёт детерминированную, чисто алгебраическую форму тезиса «оплата не бесплатна»: channel_residue, no_tax_iff_shifted, primorial_dvd_shift, shifted_primorial_bound, late_boundary_not_free. Честный вопрос: закрывает ли это программу?

Нет — и важно понять, почему. Грубого переполнения одного простого нет: у p ровно p − 2 канала, как и у carrier. Настоящий рычаг — совместность по всем q < p, то есть shifted-primorial, и она загоняет всё в единственный количественный вопрос: сколько активных $a \le A^\kappa$ имеют большой shifted-gcd $\gcd(a - \theta,\, P_{<p})$? Стресс-тест харнесса даёт неприятный ответ:

`D`	`A=70, p=29`	`A=130, p=31`	`A=240, p=37`
`p²`	0.031	0.074	0.128
1000	0.027	0.074	0.147
100	0.099	0.262	0.526

Доля $\mathrm{frac}(\gcd \ge p^2)$ растёт с масштабом (3% → 7% → 13%). Два бюджета — shifted-charge и tax — тянут в противоположные стороны и не закрываются одновременно distribution-free:

если shifted-charge мал (нужен большой порог D), то «налоговая» часть $\gcd < D$ — почти всё, но её ёмкость теряется лишь как

$$ \prod_{q \le A} \frac{q-2}{q-1} \;\sim\; \frac{1}{\ln A} \tag{17.2} $$

(Мертенс: расходимость $\sum 1/q$) — то есть суммарная потеря ёмкости по малым простым исчезающе медленная; - если мал налог (малый D), то shifted-charge $\ge 13\%$ и продолжает расти.

Итог раздела. Нет такого D = D(A), при котором оба бюджета одновременно o(|S_0|) без обращения к распределению.

Гипотеза 17.10 (единственный открытый вход маршрута оплаты). Существует функция D(A), при которой и shifted-charge, и tax одновременно составляют o(|S_0|) на реальном интервале масштаба A. «Вход» здесь — в домовом смысле: честно названное недоказанное утверждение-гейт (см. словарь).

План закрытия. Требуется корреляция сдвига a - θ с примориалом P_{<p} сильнее средней: нужно показать, что доля активных a с большим shifted-gcd мала не в среднем, а на конкретном евклидовом множестве S_0. Это ровно распределение делителей сдвига — территория Бруна/Сельберга (сито) и контроля остатка на реальном интервале (Бомбьери–Виноградов). То есть красная линия чётности, а не элементарная алгебра.

Мы не выдаём эту редукцию за доказательство: суммарная потеря ёмкости $\sim 1/\ln A$ (Мертенс) — это стена, и distribution-free её пробить нельзя.

Итог и мост к главе 18¶

Алгебра оплаты — лучшая на сегодня форма тезиса «оплата не бесплатна»: детерминированная, алгебраическая, в основном доказанная (пять теорем со стандартными аксиомами). Она не обходит стену чётности, но точно её картографирует: единственный распределительный вход изолирован в один скаляр D(A) — баланс shifted-charge против tax. Закон дефекта зафиксирован окончательно; количественный бюджет остаётся явным открытым входом — как и H у four-corner из главы 16, это та же parity-стена, но с более алгебраического ракурса.

Отсюда естественный следующий шаг. Если счётный баланс D(A) упирается в Мертенса, то, возможно, победа лежит не в счёте, а в структуре родословной активного простого — в том, что a пришло из descent клинового центра, а не взято случайно.

В главе 18 мы совершаем именно этот сдвиг стратегии: через rank descent (ранг — «высота» состояния, строго падающая вдоль разрешённых шагов; см. словарь) все product-state дефекты сводятся к rank-1, а rank-1 — к единственной, по построению не счётной лемме SNOL о терминальном сдвинутом соседе $p \mid a - 2\varepsilon$. Там, где маршрут оплаты тайно звал распределение, SNOL его запрещает и требует евклидову родословную a.