Глава 6. Явная формула фон Мангольдта

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

Глава 13.5 дала нули дзеты; Глава 13.1 — простые. Эта глава соединяет их явной формулой — математическим сердцем аналитической теории чисел, которое говорит: распределение простых есть линейный рост минус колебания, задаваемые нулями дзеты. Мостом служит функция фон Мангольдта.

Функция фон Мангольдта. Классически

$$\Lambda (n)=\{\begin{array}{ll}\log p,& n=p^k(p\text{ простое},k\ge 1),\\ 0,& \text{иначе.}\end{array}$$

Например $\Lambda (2)=\log 2$, $\Lambda (4)=\log 2$ (ибо $4=2^2$), $\Lambda (6)=0$, $\Lambda (9)=\log 3$. Эта функция «концентрирует» простые: она ненулевая ровно на степенях простых.

Что машинно проверено. Логарифм над $Q$ недоступен напрямую, поэтому в нашей арифметической основе формализована мультипликативная версия — ${\Lambda }_{\exp }(n)$, равная $p$ при $n=p^k$ и $1$ иначе (это $e^{\Lambda (n)}$, но без обращения к настоящей экспоненте). Главное — тождество

$$\prod _{d\mid n}{\Lambda }_{\exp }(d)=n,$$

которое есть в точности мультипликативная (экспоненцированная) форма классического ${\sum }_{d\mid n}\Lambda (d)=\log n$.¹

Суммарная функция $\psi (x)$

Суммарная функция фон Мангольдта —

$$\psi (x)=\sum _{n\le x}\Lambda (n)=\sum _{p^k\le x}\log p.$$

Связь с PNT. Теорема о распределении простых эквивалентна $\psi (x)\sim x$ при $x\to \infty$ — «логарифмический счёт простых» асимптотически равен $x$. Это удобная для аналитики форма PNT.

В репозитории рациональная сторона счёта простых машинно проверена: счётчик простых $‘prim{e}_{c}ount‘N=|\text{решето до }N|$ и чебышёвская сумма $‘chebyshe{v}_{t}heta‘N={\sum }_{p\le N}{\log }_{\text{прибл}}(p)$.² Само $\psi (x)\sim x$ (а с ним PNT) в этом томе не доказывается — мы располагаем рациональными счётчиками и связкой к нулям, а полную асимптотику оставляем классической.

Логарифмическая производная дзеты

Связь дзеты с $\Lambda$ даёт логарифмическая производная:

$$-\frac{{\zeta }^{\prime }(s)}{\zeta (s)}=\sum _{n\ge 1}\frac{\Lambda (n)}{n^s}(\Re s>1).$$

Это ряд Дирихле с коэффициентами $\Lambda (n)$ — прямая связь дзеты и функции фон Мангольдта. Выводится логарифмированием произведения Эйлера (Глава 13.3):

$$\log \zeta (s)=-\sum _p\log (1-p^{-s})=\sum _p\sum _{m\ge 1}\frac{p^{-ms}}{m},$$

и дифференцированием.

В ToS машинно проверена рациональная сторона логарифмирования произведения Эйлера: конечные частичные суммы ряда ${\sum }_{m\ge 1}\frac{x^m}{m}$ (который классически представляет $\log \frac{1}{1-x}$) и сумм ${\sum }_p{\sum }_m{p}^{-ms}/m$, с положительностью и монотонностью.³

Явная формула фон Мангольдта

Классическая аналитическая формула имеет вид:

$$\psi (x)=x-\sum _{\rho }\frac{x^{\rho }}{\rho }-\log (2\pi )-\frac{1}{2}\log (1-x^{-2}),$$

где сумма — по всем нетривиальным нулям $\rho$ дзеты (с симметризацией $\rho \to \bar{\rho }$). Формула поразительна: она прямо говорит

$$\text{«распределение простых»}=\text{«линейный рост }x\text{»}-\text{«колебания от нулей дзеты»}.$$

Главный член $x$ даёт $\psi (x)\sim x$ (PNT); каждый нуль $\rho$ вносит колебательный член $-x^{\rho }/\rho$.

В ToS формализована усечённая, вычислимая форма явной формулы: на каждом уровне $K$ сумма вкладов нулей конечна, рациональна и вычислима.⁴ Это и есть операциональная суть: явную формулу мы читаем как процесс приближения — конечную сумму вкладов нулей до уровня $K$, а не как завершённое суммирование по всем $\rho$.

Геометрическая интерпретация: нули управляют отклонениями

Нули дзеты «управляют» отклонениями распределения простых от среднего. Если Гипотеза Римана верна (все нули на $\Re s=1/2$):

• колебательные члены имеют $|x^{\rho }|=x^{1/2}$;
• их сумма — порядка $x^{1/2}\log x$ (после симметризации);
• значит $\psi (x)=x+O\left(x^{1/2}\log x\right)$ — оптимальная оценка остатка в PNT.

Если же RH нарушена (есть нуль с $\Re \sigma >1/2$), соответствующий член имеет $|x^{\rho }|=x^{\sigma }>x^{1/2}$, и оценка остатка ухудшается. Иначе говоря,

Гипотеза Римана$=$оптимальная асимптотика простых чисел.

Это — классическое чтение (мы его не доказываем): связь положения нулей с точностью PNT. Операционально важно, что механизм прозрачен — чем ближе нули к критической прямой, тем меньше колебания; явная формула делает «нули$\leftrightarrow$простые» явной зависимостью, а не загадкой.

Что доказано: честная сводка по ярусам

Соберём статус формализации Части XIII по ярусам прочности (это предвестие карты границ из 13.7):

• Доказано, 0 аксиом (рациональные/алгебраические/счётные ядра): определения частичных сумм дзеты и рациональные телескопические оценки; конечный эйлеров слой; лог-разложение (LogZeta); алгебраическое тригонеравенство $2(1+x{)}^2\ge 0$ над $Q$; рациональное ядро свободной зоны; грубая оценка счёта нулей; счётчики простых и чебышёвская сумма (PrimeSumBounds); экспоненцированная von Mangoldt и тождество ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)=n$ (новый слой, локально).
• С classic (L3): Cauchy-оформление дзеты/эйлерова процесса; усечённая явная формула (ExplicitFormula); синтезы свободной зоны и фаз 1/2.
• Принятая аксиома: функциональное уравнение (functional_ equation_ structure).
• Классическое чтение (не формализовано как завершённое): полная комплексная дзета и аналитическое продолжение; полный эйлеров и логарифмический комплексный слой; зона де ла Валле-Пуссена; настоящая $N(T)$ и формула Римана–фон Мангольдта; полная явная формула; PNT; сама Гипотеза Римана.

Корпус src/zeta/ — внушительный объём формализации аналитической теории чисел (точные счётчики — по текущему build accounting); но честность важнее объёма: мы строго разделяем доказанное ядро, аксиомный ярус и классическое чтение.

Разбор E/R/R: $\Lambda$-селектор и формула-связка

Правила (L5). Конституирующие правила — отбор простых степеней (функция $\Lambda$ ненулевая лишь на $p^k$; машинно — её экспоненцированная форма с тождеством ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)=n$) и связка нули$\leftrightarrow$простые (явная формула: $\psi (x)=x-{\sum }_{\rho }{x}^{\rho }/\rho$). Логарифмирование произведения Эйлера — правило перехода от простых к ряду Дирихле с $\Lambda$.

Роли (L4). «$\Lambda$» — роль-селектор (изолирует простые-степенной скелет числа); «$\psi (x)$» — роль-счётчик (логарифмический вес простых до $x$); «вклад нуля $x^{\rho }/\rho$» — роль-колебание; «явная формула» — роль-связка между нулями и простыми.

{

Элементы (L1$+$P4). Конкретные данные: значения ${\Lambda }_{\exp }(n)$, произведения ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)$, рациональные $‘chebyshe{v}_{t}heta‘N$, усечённые $‘explici{t}_{f}ormul{a}_{l}evel‘(K,x)$. Не элементы: завершённая сумма по всем нулям, полная аналитическая $\psi (x)$, ряд $-{\zeta }^{\prime }/\zeta$ как комплексный объект.}

Компонент	Что фиксирует	E/R/R-категория
отбор $p^k$ (${\Lambda }_{\exp }$, ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)=n$); связка явной формулы	конституцию связи нули$\leftrightarrow$простые	Правило (L5)
\Lambda$${}={}селектор; \psi$${}={}счётчик; x^{\rho}/\rho$${}={}колебание; формула$=$связка	статус объектов в связи	Роль (L4)
${\Lambda }_{\exp }(n)$; chebyshev_theta; explicit_formula_level	носители на каждой стадии	Элемент (L1$+$P4)

Что снимает разбор. Явная формула часто звучит как загадочная связь «откуда нули знают о простых». ToS читает её как правило-связку, рациональное ядро которого (отбор простых степеней, усечённые вклады) машинно проверяемо, а полная аналитическая форма честно остаётся классическим чтением. Функция $\Lambda$ при этом — не магический коэффициент, а селектор простых-степенного скелета, прямо вырастающий из факторизации Главы 13.1.

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

Функция фон Мангольдта прочитана как селектор простых степеней (машинно — её экспоненцированная форма с тождеством ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)=n$, прямой мост к факторизации из 13.1); явная формула — как правило-связка нулей и простых, чьё рациональное усечённое ядро формализовано, а полная аналитика оставлена классической. Статус всей части собран по ярусам.

Дальше — Глава 13.7: три эквивалентные формы Гипотезы Римана, их машинно проверенная эквивалентность, и карта границ части, окончательно разделяющая доказанное ядро, аксиомный ярус, континуальную цену и открытость RH.

---

---

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

Навигация: ← Глава 5. Нули дзеты и свободная от нулей зона · Глава 7. Гипотеза Римана: три формы и карта границ →

Footnotes

1. Новый слой src/numbertheory/VonMangoldt.v: Lambda_exp ($=p$ при $n=p^k$, иначе $1$), mangoldt_prod, psi_exp, и mangoldt_identity_upto_20 — тождество ${\prod }_{d\mid n}{\Lambda }_{\exp }(d)=n$ для всех $n\le 20$ (0 аксиом, по Print Assumptions). Это связывает арифметическую основу Главы 13.1 (делители, факторизация) с аналитической формулой ниже. Оговорка о воспроизводимости: слой src/numbertheory/ ещё не вошёл в основную ветку — он собран и проверен локально (входит в _CoqProject); классическая аддитивная $\Lambda$ с $\log p$ при этом — стандартное математическое чтение, а машинно проверена её экспоненцированная форма. ↩

2. src/zeta/PrimeSumBounds.v (0 аксиом сверх наследуемых): $‘prim{e}_{c}ount‘N=|‘sieve‘N|$ (например prime_count 3$=2$, prime_count 6$=3$), $‘prim{e}_{r}ecip‘N={\sum }_{p\le N}1/p$ и $‘chebyshe{v}_{t}heta‘N={\sum }_{p\le N}‘lo{g}_{a}pprox‘(p)$ — что соответствует $\theta (x)={\sum }_{p\le x}\log p$ (по простым), а не полной $\psi (x)={\sum }_{p^k\le x}\log p$ (по простым степеням). Это рациональные/целочисленные суммы; асимптотика $\psi (x)\sim x$ (то есть PNT) — классический результат, не доказываемый здесь. ↩

3. src/zeta/LogZeta.v (в шапке: «AXIOMS: none», 0 аксиом): log_series_term, log_series_partial, prime_power_sum, log_zeta_approx — рациональные частичные суммы ряда, классически представляющего $\log (1/(1-x))$, с неотрицательностью и монотонностью (настоящей функции log в файле нет). Переход к комплексной формуле $-{\zeta }^{\prime }(s)/\zeta (s)={\sum }_n\Lambda (n)/n^s$ требует дифференцирования, комплексного логарифма и аддитивной $\Lambda$ — это классический аналитический слой, здесь не формализованный. ↩

4. src/zeta/ExplicitFormula.v (в шапке: «AXIOMS: classic, inherited from ZetaProcess»): zero_contribution$(\beta ,x)$ — рациональный вклад $x^{\beta }$, explicit_formula_level$(K,x)$ — усечение явной формулы на уровне $K$ (вычислимо: explicit_formula_computable), pole_correction, explicit_formula_step. Это усечённый процессный вариант, наследующий classic; полная классическая явная формула $\psi (x)=x-{\sum }_{\rho }{x}^{\rho }/\rho -\dots$ — аналитическое чтение поверх него. ↩