14. Модель против реальности: остаток

← 13. Фрактальный слой · Оглавление · 15. Цепь к близнецам →

Lean: EuclidsPath/Engine/RealFourCorner.lean (real_four_corner_decomp, real_four_corner_of_remainder). Численный замер: tools/RESULTS_remainder.md.

В предыдущей главе 13 мы выстроили фрактальный слой двигателя и показали, что направление R_fc ≤ 1 форсируется не плотностью простых, а эксклюзивностью двойки: на каждом простом вклад в ранги (r_-, r_+) исключающий, отчего производящая функция рангов есть произведение ∏_p (c_p + a_p x + b_p y) без перекрёстного члена xy. Это дало модельный four-corner.

Но модель — не реальность. В настоящей главе мы честно разделяем эти две вещи: вводим точную декомпозицию реального four-corner на модельную часть и остаток, выписываем тождество остаточного члена, и показываем, где именно вся программа упирается в один-единственный узел — контроль знака остатка.

Модель и реальность: две системы счётов

Напомним постановку. Мы работаем с ранговыми счётами N_{ij} — числом carrier-центров данного слоя, у которых сторона 6m-1 имеет ранг (число различающих малых делителей) i, а сторона 6m+1 — ранг j. Four-corner есть неравенство

\[ N_{00}\, N_{33} \;\le\; N_{03}\, N_{30}, \tag{14.1} \]

означающее отрицательную ассоциацию рангов: «оба высоких» реже, чем «наперекрёст».

У нас имеется две реализации этих счётов.

Определение 14.1 (модельные счёты). Модельные счёты N_{ij}^{CRT} порождаются CRT-генфункцией ∏_q G_q, G_q = c_q(1 + w_q(x+z)), w_q = 1/(q-2). Они факторизуются по простым и по построению удовлетворяют модельному four-corner (ModelFourCorner, model_four_corner), сводящемуся к биномиальному тождеству \(20\cdot C(n,6) \le C(n,3)^2\) (four_corner_binom).

Определение 14.2 (реальные счёты). Реальные счёты N_{ij}^{real} — это фактические счёты, полученные просеиванием (сито), без предположения о независимости простых.

Модельные счёты мы доказали элементарно; реальные — то, что нам действительно нужно. Разница между ними — единственное, что стоит между машинно-проверенным маршрутом и гипотезой близнецов.

Определение 14.3 (ситовый остаток). Для каждого угла (i,j) положим

\[ e_{ij} \;:=\; N_{ij}^{real} - N_{ij}^{CRT}. \tag{14.2} \]

Остаток e_{ij} есть целое число произвольного знака (реальность может как недосчитывать, так и перебирать модель).

Ключевое дисциплинарное требование: e_{ij} ∈ ℤ без предположений о знаке или малости. Всё, что мы позволяем себе делать с остатком, — кольцевая алгебра над ℤ. Ни анализа, ни распределения, ни оценок сита.

Точная декомпозиция

Обозначим для краткости модельные счёты четырёх углов m00 = N_{00}^{CRT}, m03, m30, m33 и соответствующие остатки e00, e03, e30, e33. Реальный счёт каждого угла есть m + e. Подставим это в реальный four-corner и раскроем.

Теорема 14.4 (real_four_corner_decomp). Для любых целых m00, m03, m30, m33, e00, e03, e30, e33

\[ (m_{00}+e_{00})(m_{33}+e_{33}) - (m_{03}+e_{03})(m_{30}+e_{30}) \]

\[ =\; \underbrace{(m_{00}m_{33} - m_{03}m_{30})}_{\text{модельная разность } \Delta_{model}} \;+\; \underbrace{(m_{00}e_{33} + e_{00}m_{33} + e_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} - e_{03}e_{30})}_{\text{остаточный член } R}. \tag{14.3} \]

В Lean это чистое кольцевое тождество, закрываемое тактикой ring. Никакой геометрии, никакого сита — только раскрытие скобок. Значение теоремы в том, что она точна: это не приближение и не оценка, а тождество. Реальная разность four-corner в точности равна модельной разности плюс явно выписанный остаточный член R.

Примечание. Обратим внимание на структуру R. Он распадается на три группы. Линейные по остатку кросс-термы m_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} + e_{00}m_{33} — это первый порядок отклонения реальности от модели. Квадратичные термы e_{00}e_{33} - e_{03}e_{30} — это «four-corner самого остатка». Именно поэтому мы не можем просто оценить R покомпонентно: он смешивает модель и остаток, и его знак зависит от корреляции между углами.

Сведение: реальный four-corner из модельного плюс контроль остатка

Тождество даёт нам чёткое условие, при котором реальный four-corner следует из модельного. Модельную часть Δ_{model} = m_{00}m_{33} - m_{03}m_{30} мы контролируем: модельный four-corner — это \(m_{00}m_{33} \le m_{03}m_{30}\), то есть \(Δ_{model} \le 0\), а модельный запас есть \(m_{03}m_{30} - m_{00}m_{33} = -\Delta_{model} \ge 0\). Тогда реальный four-corner выполнен ровно тогда, когда остаток укладывается в этот запас.

Теорема 14.5 (real_four_corner_of_remainder). Пусть выполнен модельный four-corner

\[ m_{00}\, m_{33} \;\le\; m_{03}\, m_{30} \qquad (\text{гипотеза } \verb|_hmodel|), \]

и остаточный член укладывается в модельный запас

\[ R \;=\; m_{00}e_{33} + e_{00}m_{33} + e_{00}e_{33} - m_{03}e_{30} - e_{03}m_{30} - e_{03}e_{30} \;\le\; m_{03}m_{30} - m_{00}m_{33} \qquad (\text{гипотеза } \verb|hrem|). \]

Тогда выполнен и реальный four-corner:

\[ (m_{00}+e_{00})(m_{33}+e_{33}) \;\le\; (m_{03}+e_{03})(m_{30}+e_{30}). \]

Доказательство в Lean прямолинейно: подставляем декомпозицию из Теоремы 14.4 (real_four_corner_decomp), из гипотезы hrem заключаем, что реальная разность \(\le 0\) (через linarith), откуда неравенство. Логически теорема утверждает ровно то, что мы и хотели: реальный four-corner ⟺ модельный four-corner (доказан) + одно неравенство на остаток.

Вывод. Это и есть честная граница программы, выписанная в виде одной формулы. Мы не спрятали трудность — мы её локализовали. Всё математическое содержание гипотезы близнецов, оставшееся незакрытым в этой ветви, сжато в единственную гипотезу hrem: остаток не должен переворачивать знак модельного four-corner, то есть не должен вырасти настолько, чтобы выскочить за модельный запас \(-\Delta_{model}\).

Примечание. Подчеркнём, что Теорема 14.5 (real_four_corner_of_remainder) — это редукция, а не доказательство реального four-corner. Гипотеза hrem не доказана и в общем виде не следует из уже установленного. Выдавать эту теорему за доказательство было бы подменой: она лишь переносит бремя с «реальный four-corner» на «остаток укладывается в запас» — точную, но открытую цель.

Числа: остаток около 4× модели

Чтобы понять, насколько узок этот узел, мы прямо измерили остаток (remainder_harness.py, сводка в tools/RESULTS_remainder.md). Сравнивались реальные N_{ij}^{real} из сита с модельными \(N_{ij}^{CRT} = T\cdot\prod_q c_q \cdot C(i+j,i)\cdot e_{i+j}\) (генфункция ∏_q(1 + w_q(x+z)), w_q = 1/(q-2)).

Результат обескураживает. Остаток не мал — он огромен и систематичен:

угол	e/model, k=20	k=22	k=24
N_{00}	−17%	−18%	−18%
N_{03}, N_{30}	+85%	+85%	+87%
N_{33}	+283%	+298%	+326% (растёт)

CRT-модель недосчитывает N_{33} в 3.8–4.3 раза; остаток в высоких рангах больше самих модельных счётов. Иными словами, остаточный член R — не поправка к модели, он того же порядка (и крупнее) главного члена. Наблюдение: реальность в углу (3,3) систематически плотнее модели, и разрыв растёт с масштабом.

Теперь — держится ли запас? Сравним реальное и модельное отношения four-corner R_{fc} = N_{00}N_{33}/(N_{03}N_{30}):

	k=20	k=22	k=24
R_{fc}^{real}	0.873	0.918	0.976
\(R_{fc}^{model} = 20\,e_6/e_3^2\)	0.937	0.959	0.973

Оба отношения стремятся к 1 снизу (модельный запас \(-\Delta_{model} \to 0\)), но на k=24 они пересекаются: реальный избыток обгоняет модельный. Реальный four-corner при этом всё ещё держится (R_{fc}^{real} < 1), но модельный запас его уже не покрывает.

Примечание. Это ровно та ситуация, которую формализует hrem. Гипотеза требует \(R \le -\Delta_{model}\). Но при k=24 реальный избыток превысил модельный — то есть эмпирически R уже не укладывается в модельный запас. Реальный four-corner держится по другой, немодельной причине.

Где узел открыт: гипотеза и план закрытия

Итог раздела. Численный вывод однозначен: перенос модель→реальность в distribution-free стиле через оценку остатка модельным запасом не работает. Остаток около 4× модели и обгоняет исчезающий модельный запас. Реальный four-corner держится, но не благодаря модельной конструкции — а значит, за его устойчивостью стоит нечто, чего CRT-модель не видит. Это и есть проблема чётности: гипотеза hrem, как она сформулирована (через модельный запас), недостижима.

Гипотеза 14.6 (открытый узел). Реальный four-corner \(N_{00}^{real} N_{33}^{real} \le N_{03}^{real} N_{30}^{real}\) держится на сколь угодно больших масштабах. Эквивалентно (по Теореме 14.4 (real_four_corner_decomp)): остаточный член R не переворачивает знак реальной разности four-corner, то есть \(R \le -\Delta_{model}\).

План закрытия (и его граница). Наивный план — доказать hrem через модельный запас \(-\Delta_{model}\) — измерением опровергнут: запас тает быстрее, чем растёт остаток. Естественно предположить, что нужен прямой контроль знака реальной разности, не проходящий через модель: оценка R не сверху числом \(-\Delta_{model}\), а через собственную структуру остатка (эксклюзивность двойки на уровне реальных, а не модельных счётов). Здесь линия упирается в чётность: любой чисто счётный (по модельному запасу) аргумент недостаточен. По красной линии программы этот узел нельзя закрывать распределением простых или large-sieve. Если единственный доступный путь потребует именно этого — мы останавливаемся и показываем точную точку; и эта точка — гипотеза hrem, немодельная версия.

Примечание. Ценность главы не в том, что узел закрыт, — он открыт. Ценность в том, что вся нерешённая часть задачи сжата в одно точное целочисленное неравенство hrem на явно выписанный остаточный член, изолированное нециркулярно и машинно-проверенно (Теорема 14.5, real_four_corner_of_remainder). Мы знаем, что именно осталось доказать, и знаем — из чисел, — что модельный запас для этого недостаточен.

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

Итак, у нас есть точная развилка: реальный four-corner ⟸ модельный four-corner (доказан) + hrem (открыт, немоделен). В следующей главе 15 ToTwins мы собираем именно эту развилку в одну машинно-проверенную цепь: реальный four-corner плюс side-corner дают N_{33} < N_{00}, отсюда выживший carrier-центр, отсюда twin, отсюда TwinLowers.Infinite.

Реальный four-corner входит туда как открытый вход H — гейт, то есть честно названное недостающее утверждение (см. словарь); это первая точная формулировка единственного распределительного узла программы, который затем будет переосмыслен уже не как счётный, а как структурный 18 SNOL. Иначе говоря, глава 15 показывает, что hrem — не одна из многих трудностей, а та самая и единственная, к которой сводится вся ветвь.

---

← 13. Фрактальный слой · Оглавление · 15. Цепь к близнецам →