Глава 1. Простые числа в операциональной онтологии

Где стоит глава

Открытие Части XIII

Часть XII перечитала геометрию: точка оказалась роль-позицией, кривизна — угловым дефектом, многообразие — процессом измельчающейся триангуляции, а не готовой континуальной вещью. Часть XIII обращается к теории чисел и к её центральному аналитическому объекту — дзета-функции Римана. Для классического математика это, пожалуй, самая интригующая часть тома: здесь живёт Гипотеза Римана, не решённая с 1859 года, и здесь же мы аккуратно отделяем то, что доказано, от того, что принято или остаётся открытым.

Сквозная нить части коротка: дзета-функция есть процесс частичных сумм; теория простых чисел — изучение этого процесса; нули и полюс дзеты — его структурные особенности; Гипотеза Римана — открытое утверждение о структуре нулей. Всё это в ToS проводится без аксиомы выбора, через явные алгоритмические конструкции.

Прежде чем заняться дзетой (Глава 13.2), мы закладываем фундамент — простые числа. И здесь важно сразу обозначить, что в ToS простые — не точки заранее данного «множества всех простых», а роль в мультипликативном устройстве натурального ряда. Эта глава развёртывает их в четырёх сквозных мотивах части:

• [(M1)] Структурная неизбежность. Простые возникают не как один из возможных способов классификации, а как структурно неизбежные образующие — атомы.
• [(M2)] Операциональная делимость. Натуральное $n$ рассматривается на нескольких уровнях: как объект, как произведение простых, как процесс факторизации.
• [(M3)] Множество как режим. «Множество всех простых» есть режим работы, а реально простое — классификация натуральных по разрешимому предикату.
• [(M4)] Позитивная онтология. Простые делители структурно неотрицательны; кратности неотрицательны; ряды Дирихле в области сходимости работают с положительными членами.

Замечание о подтверждении. Как и во всём томе, ведущим является описание системы; Rocq-репозиторий служит подтверждением того, что конструкция машинно проверяема. Имена файлов, формулировки и числа проверенных утверждений вынесены в сноски. Для этой части мы дополнительно проверили все ссылочные числа на текущем состоянии репозитория и приводим именно их.¹

Простое число как разрешимый предикат

В ToS «быть простым» есть не свойство элемента предсуществующего множества, а правило конституции: число $n\ge 2$ просто, если его делят только $1$ и оно само. Делимость и простота задаются прямо:

Definition divides (d n : nat) : Prop := exists k, n = d * k.
 
Definition is_prime (n : nat) : Prop :=
  2 <= n /\ forall d, 2 <= d -> d < n -> ~ divides d n.

Ключевое слово здесь — разрешимость. Параллельно предикату определена булева проверка is_prime_bool, перебирающая делители в конечном диапазоне $2,\dots ,n-1$; для каждого конкретного $n$ вопрос «просто ли $n$?» решается за конечное число шагов. Отдельная функция smallest_factor ищет наименьший делитель пробным делением и останавливается уже при $d^2>n$.² Это в точности соответствует P4: простота не «считывается» с готовой бесконечной таблицы, а вычисляется на конкретном конечном носителе.

• $2,3,5,7,11,\dots$ — простые;
• $4,6,8,9,10,\dots$ — составные;
• $1$ — единица: не простое и не составное (его единственный делитель — оно само), а первый акт счёта (Часть II);
• $0$ — особый случай: оно делится на всё и не несёт мультипликативного статуса.

Уже здесь видна позиция (M3): мы не вводим «множество $\mathbb{P}$ всех простых» как завершённый объект-тотальность. Сам предикат is_prime, разумеется, вполне законен — запрещена лишь завершённая бесконечная совокупность как Элемент. Простое — это классификация натуральных по предикату; «все простые» — режим обхода этой классификации, а не предмет, лежащий целиком перед нами.

Простые как атомы: основная теорема арифметики

Что делает простые фундаментальными? Ответ — основная теорема арифметики: каждое натуральное $n\ge 1$ единственным образом (с точностью до порядка) разлагается в произведение простых. В ToS обе половины этого утверждения — существование и единственность — машинно доказаны.³

Существование как алгоритм. Разложение не постулируется, а строится: для $n\ge 2$ берётся наименьший делитель (он прост), число делится на него, и процедура повторяется. Для конкретного $n$ она завершается за конечное число шагов — это пробное деление. Представление разложения — конечный список простых, чьё произведение равно $n$.

Единственность через лемму Евклида. Сердце единственности — лемма Евклида: если простое $p$ делит произведение $a\cdot b$, то $p$ делит $a$ или $b$.⁴ Из неё следует, что два разложения одного числа суть перестановки друг друга. Так кратность каждого простого в разложении оказывается инвариантом числа — его конститутивной характеристикой.

Мотив M1. Это и есть структурная неизбежность в чистом виде. Простые — не «удобная» классификация: они единственным образом определены делимостью и являются образующими мультипликативного моноида $N$. При любом нетривиальном взгляде на натуральные числа простые возникают как фундаментальные точки. Машинно проверенная единственность факторизации — это корректность роли «атом»: атомы не только существуют, но и составляют каждое число однозначно.

Конкретный пример, проверенный вычислением: $12=2\cdot 2\cdot 3$, и любое простое разложение числа $12$ есть перестановка списка $[2;2;3]$.⁵

Бесконечность простых: алгоритм, а не завершённое множество

Знаменитейшее утверждение о простых — их бесконечность. В ToS оно получает форму, в точности отвечающую P4: не «существует бесконечное множество», а алгоритм неограниченного построения.

Теорема (Евклид, конструктивно). Для любого $N$ существует простое число, большее $N$.

Доказательство алгоритмично: рассмотрим $N!+1$. Оно $\ge 2$, значит имеет простой делитель $p$. Если бы $p\le N$, то $p$ делило бы и $N!$, и $N!+1$, а значит и их разность $1$ — невозможно. Следовательно $p>N$.⁶ Дано конечное собрание простых — мы программно строим новое.

Это и есть бесконечность в смысле P4: бесконечность есть свойство процесса, а не завершённого объекта. «Простых бесконечно много» означает «процедура построения следующего простого никогда не упирается в стену», а не «где-то лежит готовое бесконечное множество $\mathbb{P}$». Эквивалентная формулировка — «для любого $N$ есть простое $>N$» — ровно фиксирует эту неограниченность как правило, а не как объект.

Распределение простых: функция счёта

Раз простые редеют, но не исчерпываются, естественно считать их. Функция счёта $\pi (x)$ — число простых, не превосходящих $x$ — в ToS есть роль-счётчик: для каждого конкретного $x$ это конкретное число, вычисляемое за конечное время как длина решета.⁷

$x$	$\pi (x)$	\quad	$x$	$\pi (x)$
$10$	$4$		$100$	$25$
$30$	$10$		$1000$	$168$

Эмпирическая картина начальных значений показывает разрежение: на больших отрезках простых относительно меньше, при том что счётчик монотонно растёт и неограниченно (последнее — прямое следствие евклидовой бесконечности из «Бесконечность простых: алгоритм, а не завершённое множество»). Само «разрежение» как точное утверждение — уже аналитическое и относится к асимптотике ниже.

Теорема о распределении простых. Главный асимптотический результат классической теории гласит:

$$\pi (x)\sim \frac{x}{\ln x}(x\to \infty ),$$

то есть ${\lim }_{x\to \infty }\pi (x)\ln x/x=1$ (Адамар и Валле-Пуссен, 1896). В ToS это операциональное утверждение об асимптотике двух процессов — $\pi (x)$ и $x/\ln x$. В этой главе PNT не доказывается. В Главах 13.2–13.5 мы подводим операциональный аналитический механизм, через который такая асимптотика доказывается классически: дзета как процесс, произведение Эйлера, нули и свободная от нулей зона. Что именно из этого механизма машинно проверено — честно очерчено в 13.5 и в карте границ части (13.7). Здесь же важно лишь, что асимптотика простых — утверждение о поведении счётчика, а не о свойстве готового бесконечного множества.

Разбор E/R/R: простое как функциональная система

Соберём сказанное в стандартный разбор Элементы/Роли/Правила, в порождающем порядке Правила $\to$ Роли $\to$ Элементы.

Правила (L5). Конституирующее правило — делимость: простое определено как неразложимое относительно умножения (is_prime). На уровне всего ряда правило усиливается до факторизации с единственностью — основная теорема арифметики. Именно правило (а не перечень) говорит, что значит «быть атомом».

Роли (L4). Натуральное число получает мультипликативный статус: «простое» — роль атома (образующая моноида); «составное» — роль произведения атомов; «$1$» — роль единицы (пустое произведение). Число $n$ при этом многослойно (M2): объект счёта, произведение простых, процесс факторизации.

Элементы (L1$+$P4). На каждой стадии — конечные данные над $N$: конкретные простые, конечные списки делителей и разложений, значения счётчика $\pi (x)$ до конечного $x$. Не элементы: «множество всех простых», завершённая таблица простоты, бесконечное собрание разложений.

Компонент	Что фиксирует	E/R/R-категория
предикат делимости; основная теорема (существование$+$единственность)	конституцию простого и однозначность разложения	Правило (L5)
«простое»$=$атом, «составное»$=$произведение, «$1$»$=$единица	мультипликативный статус числа	Роль (L4)
конкретные натуральные; конечные списки делителей/разложений; $\pi (x)$	носители на каждой стадии	Элемент (L1$+$P4)

Проверка корректности. Каждый компонент попадает ровно в одну категорию. Роль «атом» корректна именно потому, что машинно доказана единственность факторизации: атомы составляют каждое число однозначно. Бесконечность простых корректна как правило (алгоритм построения), а не как объект.

Что снимает разбор (диагностика). Корневая категориальная ошибка — овеществление «множества всех простых» как завершённого предмета и приписывание ему свойств, доступных лишь конечным данным. ToS разводит уровни: простое — роль (атом); «все простые» — режим обхода (M3); бесконечность — правило неограниченного построения (P4). Это та же дисциплина, что позволила Части IV не путать процесс с завершённым континуумом; здесь она прилагается к мультипликативной структуре $N$.

Простые и квантовый хаос: мост в Том III

Одна из самых поразительных связей современной математической физики стоит упомянуть уже здесь, хотя её развёртывание — дело Тома III. Изучая расстояния между нетривиальными нулями дзеты, Хью Монтгомери (1973) заметил статистическое совпадение с распределением расстояний между собственными значениями случайных эрмитовых матриц (Gaussian Unitary Ensemble, GUE) — модели спектров сложных квантовых систем. Связь не доказана, но численно подтверждена для триллионов вычисленных нулей.

Отсюда — гипотеза Гильберта–Полиа: нули дзеты суть собственные значения некоторого самосопряжённого оператора, «квантового гамильтониана числовой теории». Такой оператор не найден, и его поиск — активная область. В операциональном прочтении это обратная задача: дано распределение спектра (нули дзеты), требуется оператор. Мы фиксируем здесь лишь философскую рамку: если картина верна, распределение простых есть классический след некоторой квантовой системы, а нули дзеты — её энергетические уровни. Никакой формализации этой связи мы не предъявляем; в репозитории ей соответствует лишь аналогия «нули $\leftrightarrow$ нули статистических сумм», проводимая отдельно.⁸ Подробное обсуждение — в Томе III.

Что глава подготовила

Простые установлены как атомы мультипликативного устройства $N$ — роль, корректность которой гарантирована машинно проверенной основной теоремой арифметики; их бесконечность прочитана как алгоритм (P4), а распределение — как поведение счётчика $\pi (x)$. Эта элементарная основа — то, что классическая аналитическая теория чисел обычно молчаливо предполагает; здесь она развёрнута как конечная операциональная программа и машинно проверена с нуля (0 аксиом, по Print Assumptions).

Дальше:

• Глава 13.2 — дзета-функция как процесс частичных сумм;
• Глава 13.3 — произведение Эйлера, связывающее дзету с простыми (и опирающееся в точности на единственность факторизации из «Простые как атомы: основная теорема арифметики»);
• Глава 13.4 — функциональное уравнение и критическая прямая;
• Глава 13.5 — нули и свободная от нулей зона (аналитический механизм, через который классически доказывается асимптотика из «Распределение простых: функция счёта»);
• Глава 13.6 — явная формула фон Мангольдта;
• Глава 13.7 — три эквивалентные формы Гипотезы Римана и карта границ части.

---

---

Часть: Часть XIII. Дзета-функция и теория чисел · Том: «Математика»

Навигация: ← Глава 6. Синтез и карта границ — Часть XII · Глава 2. Дзета-функция как процесс →

Footnotes

1. Элементарная теоретико-числовая основа этой главы собрана в каталоге src/numbertheory/ (9 файлов, 138 Qed, 0 Admitted, 0 аксиом — все утверждения проходят Print Assumptions как «Closed under the global context»). Глава 13.1 опирается на stdlib/Primes.v (21 Qed), PrimeFactorization.v (21 Qed), EuclidInfinitude.v (5 Qed) и PrimeCounting.v (9 Qed). ↩

2. stdlib/Primes.v: divides, divides_bool, is_prime, is_prime_bool (перебор $2,\dots ,n-1$), решето sieve, smallest_factor (остановка при $d^2>n$). Машинно проверено, что is_prime_bool даёт true на $2,3,5$ и false на $0,1,4$; решето sieve 8 вычисляется в $[2;3;5;7]$. В самом Primes.v имеются частичные reflection-леммы prime_ge_2 и prime_not_composite; полная лемма рефлексии is_prime_bool_true_is_prime (булев результат влечёт пропозициональную простоту) доказана в PrimeFactorization.v и используется ниже. ↩

3. PrimeFactorization.v: factor_exists (существование разложения — сильная индукция по $n$), prime_factorization_unique (единственность до перестановки, формализованной типом Permutation), и fundamental_theorem_of_arithmetic, объединяющая обе. 21 Qed, 0 аксиом. ↩

4. euclid_lemma в PrimeFactorization.v. Доказана через стандартный теоретико-числовой факт Nat.gauss (если $\gcd (p,a)=1$ и $p\mid a\cdot b$, то $p\mid b$), с мостом между репозиторной делимостью divides и библиотечной Nat.divide. Из неё индукцией по списку выводится, что простое, делящее произведение простых, совпадает с одним из них, а отсюда — единственность факторизации как перестановочная эквивалентность двух списков. ↩

5. factorization_12 и factorization_12_unique в PrimeFactorization.v. ↩

6. EuclidInfinitude.v: exists_larger_prime (для всякого $N$ существует простое $>N$, через простой делитель $N!+1$; вспомогательная divides_fact: всякое $1\le d\le n$ делит $n!$), и primes_not_finite (никакой конечный список не содержит всех простых). 5 Qed, 0 аксиом. Опирается на exists_prime_divisor из PrimeFactorization.v. ↩

7. PrimeCounting.v: pi x := length (sieve x); машинно проверено $\pi (10)=4$, $\pi (30)=10$, $\pi (100)=25$, $\pi (1000)=168$; доказаны характеризация принадлежности решету (in_sieve_iff) и монотонность (pi_monotone). 9 Qed, 0 аксиом. ↩

8. src/zeta/LeeYangAnalogy.v проводит структурную аналогию между нулями дзеты и нулями статистических сумм (Ли–Янг); это аналогия, а не доказательство гипотезы Монтгомери или Гильберта–Полиа. ↩