Глава 4. Процессная экспонента exp

Замысел главы и смена яруса

Формальное сердце Главы 16.3 — тождество $e^{- l n (1 - x)} = 1/ (1 - x)$ — было получено на коэффициентах: как равенство формальных рядов. Чтобы перенести его в равенство чисел-процессов (в каждой точке $∣ x ∣ < 1$ ), нужен инструмент, которого у нас ещё нет: экспонента, умеющая брать в аргумент не рациональное число, а целый процесс — вещественную экспоненту $exp_{R} : ‘ C a u c h y S e q ‘ \to ‘ C a u c h y S e q ‘$ . Эта глава её строит.

И здесь честно отметим смену яруса. Главы 16.1–16.3 жили на 0-аксиомной, чисто формальной стороне: всё было конечной арифметикой коэффициентов. Начиная с этой главы мы входим в аналитический слой — слой Коши-вещественных, где работают пределы. Аналитические оценки сами по себе аксиомо-свободны, но вся конструкция вещественной экспоненты опирается на закон исключённого третьего L3. Это первый ярус Части XVI, где появляется L3, и мы помечаем его прямо: сноски здесь говорят не <<0 аксиом>>, а <<без новых аксиом, только L3>>.

Дорога такая. Сперва — движок: теорема Мертенса о произведении рядов, конструктивно над $Q$ (§ 16.4.2). На ней — рациональная экспонента как гомоморфизм групп: теорема сложения, единица, обратимость (§ 16.4.3). Затем — экспонента процесса $exp_{R}$ , через диагональный предел (§ 16.4.4). И наконец — её гомоморфизм групп на вещественных и инъективность, с двумя собственными приёмами (§ 16.4.5). Разбор E/R/R и переход к мосту Главы 16.5 завершают главу (§ 16.4.6).

Движок: теорема Мертенса

Чтобы экспонента была мультипликативной — $exp (u + v) = exp (u) exp (v)$ , — нужно уметь перемножать ряды как пределы. Общий принцип Мертенса: произведение Коши двух сходящихся рядов сходится к произведению их пределов,

(i \sum a_{i}) (j \sum b_{j}) = n \sum (i + j = n \sum a_{i} b_{j}) .

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

В нашей системе она построена конструктивно над $Q$ — без обращения к библиотечному типу вещественных чисел Rocq, как равенство процессов. <<Конструктивно над $Q$ >> здесь значит, что сами оценки и конечные алгебраические тождества выполняются над рациональными порогами и частичными суммами; переход от них к равенству Коши-процессов уже использует L3. Содержательный шаг — разностное тождество, превращающее неуправляемую вне-диагональную часть $A_{n} B_{n} - C_{n}$ в блочную сумму, которую можно оценить хвостами Коши; капстоун — $ε /2$ -аргумент по двум порогам. Этого движка в библиотеке не было — вспомогательное расщепление частичной суммы автор когда-то оставил недоказанным; здесь оно воскрешено и доведено до полной теоремы.¹

Рациональная экспонента: сложение и гомоморфизм групп

Первое применение Мертенса — теорема сложения экспоненты на рациональном аргументе:

exp (u + v) \sim exp (u) \cdot exp (v)

(здесь $\sim$ — равенство чисел-процессов). Доказательство сводит весь анализ к одному покоэффициентному тождеству: свёртка экспоненциальных рядов в точках $u$ и $v$ есть экспоненциальный ряд в точке $u + v$ . А оно — чистая конечная алгебра: конволюционная рекуррентность $(n + 1) c_{n + 1} = (u + v) c_{n}$ , то есть факториальная форма биномиального тождества без самих биномиальных коэффициентов.²

С двумя спутниками теорема сложения превращает экспоненту в гомоморфизм групп. Единица: $exp (0) \sim 1$ . Обратимость: $exp (- u)$ есть обратный к $exp (u)$ , ибо $exp (u) \cdot exp (- u) \sim 1$ .³ Три равенства-процесса вместе,

exp (u + v) \sim exp (u) \cdot exp (v), exp (0) \sim 1, exp (u) \cdot exp (- u) \sim 1,

говорят, что экспонента ведёт себя как гомоморфизм из аддитивной группы рациональных $(Q, +, 0, -)$ в мультипликативную группу обратимых Коши-процессов (это и есть положительные вещественные $R^{+}$ как процессная структура) — сложение переходит в умножение, нуль в единицу, отрицание в обращение. Это тот самый канонический гомоморфизм, который Часть XI (алгебра) знает абстрактно; здесь он построен явно, над процессами — как набор доказанных групповых тождеств (отдельного носителя $R^{+}$ мы при этом не вводим).

Экспонента процесса: $exp_{R}$ {exp_R}

Пока экспонента берёт в аргумент рациональное число. Но вещественное число в нашей системе — это процесс $P : N \to Q$ (Часть IV). Чтобы взять экспоненту от вещественного, нужна $exp_{R}$ , аргумент которой — целый процесс.

Строится она диагональю. Каждое рациональное приближение $P n$ даёт число-процесс $exp (P n)$ ; получается последовательность процессов, и её диагональ

exp_{R} (P) := diag_{n} exp (P n)

есть снова один Коши-процесс — при условии, что последовательность процессов мета-Cauchy.

Definition exp_R (P : CauchySeq) : CauchySeq :=
  diagonal_limit (fun n => exp_limit (P n)) (exp_meta_cauchy P).

Мета-Cauchy держится на двух равномерных опорах (процесс $P$ ограничен числом $B$ ). Первая — равномерный хвост экспоненциального ряда: для всех аргументов модуля $\leq B$ хвост ряда мал единообразно. Вторая — липшицевость по аргументу: близкие аргументы дают близкие частичные суммы, потому что $∣ a^{k} - b^{k} ∣ \leq k B^{k - 1} ∣ a - b ∣$ (телескоп степеней). Аналитическое ядро этих оценок — аксиомо-свободно.⁴ Это и есть та вещественная экспонента, которой в системе не было: прежняя $exp$ умела брать лишь рациональный аргумент. Образ P4: каждое $exp (P n)$ уже есть число-процесс, а $exp_{R} (P)$ берёт диагональный предел по этим процессам — то есть role-limit последовательности role-limit’ов (процесс процессов), сведённый полнотой к одному Коши-процессу.

Гомоморфизм и инъективность

Вещественная экспонента наследует структуру рациональной — и добавляет к ней инъективность.

Теорема сложения держится и на процессах: $exp_{R} (P + R) \sim exp_{R} (P) \cdot exp_{R} (R)$ . Доказать её <<произведением диагоналей>> нельзя — на пополнении нет непрерывности умножения. Приём иной — диагональный Мертенс: на диагонали $n$ разность $Σ exp (P_{n}) \cdot Σ exp (R_{n}) - Σ exp (P_{n} + R_{n})$ есть мертенсовский блок, ограниченный равномерными мажорантами. Вместе с единицей и обратимостью это даёт полный гомоморфизм групп уже на вещественных.⁵

Инъективность: $exp_{R} (A) \sim exp_{R} (B) \Rightarrow A \sim B$ . Здесь конструктивная тонкость: частичные суммы экспоненты от отрицательного аргумента не монотонны, и наивная оценка не проходит. Приём — regime-free: всё сводится к ядру $exp_{R} (D) \sim 1 \Rightarrow D \sim 0$ , а оно решается без квадратичного хвоста — из $exp_{R} (D) \sim 1$ выводится и $exp_{R} (- D) \sim 1$ (через обратимость), затем знаковое расщепление $D$ с монотонной нижней оценкой $1 + t \leq \sum exp -term t$ (при $t \geq 0$ ), применённой к $D$ и к $- D$ .⁶

Инъективность — последний рычаг к Главе 16.5: именно она позволит из равенства экспонент заключить равенство аргументов, замкнув функциональное уравнение логарифма.

Разбор E/R/R, ярус и что глава готовит

компонент главы	роль в системе	слой E/R/R
члены $exp$ -ряда и их частичные суммы	носители, конечны на стадии $n$	Element (P4)
$exp_{R}$ — экспонента процесса	роль-функция (вещественная $exp$ )	Role
теорема сложения, гомоморфизм групп	роль-гомоморфизм $(+) \to (\cdot)$	Role
Мертенс, диагональный Мертенс, regime-free инъективность	процесс-оценки	Rule (L3)

Elements. На каждой стадии $n$ — конечные рациональные частичные суммы экспоненциального ряда и конечные свёртки. Element-сторона цела.

Roles. $exp_{R}$ играет роль вещественной экспоненты; теорема сложения — роль гомоморфизма аддитивной группы $(Q, +)$ в мультипликативную группу обратимых Коши-процессов; Мертенс — роль движка, переносящего покоэффициентную свёртку в предельное равенство.

Rules. Конволюционная рекуррентность, диагональный Мертенс, regime-free инъективность — правила, по которым процесс-оценки собираются в теоремы.

Диагностика P4 и ярус. $exp_{R} (P)$ — role-limit последовательности процессов, сведённый полнотой к одному Коши-процессу: вещественное = процесс, экспонента вещественного = role-limit процессов. И здесь честная пометка яруса: в отличие от 0-аксиомного формального исчисления Глав 16.1–16.3, этот слой опирается на L3 (закон исключённого третьего). Аналитические оценки (липшиц степеней, равномерный хвост, разностное тождество Мертенса) аксиомо-свободны; но вся конструкция вещественной экспоненты и теоремы сложения — только L3, без иных аксиом.⁷

Что нового. Теорема Мертенса, теорема сложения экспоненты, её инъективность — классический анализ. Ново — их конструктивно-над- $Q$ прочтение как равенств процессов (без обращения к библиотечному типу вещественных чисел Rocq), два собственных приёма (диагональный Мертенс и regime-free инъективность) и заполнение реального пробела системы: вещественной экспоненты-процесса и движка Мертенса прежде не было. Уровень — новое обрамление и методы.

Что глава готовит. У нас есть вещественная экспонента $exp_{R}$ с теоремой сложения и инъективностью — и формальное сердце $e^{- l n (1 - x)} = 1/ (1 - x)$ из Главы 16.3. Глава 16.5 соединяет их: мост вычисления переносит покоэффициентное тождество в число-процесс, теорема Таннери склеивает диагональ $exp_{R}$ с этим вычислением, и получается ключ $exp_{R} (ln- процесс) \sim 1/ (1 - x)$ — из которого инъективность и гомоморфизм замыкают функциональное уравнение логарифма.

Часть: Часть XVI. Функция как процесс · Том: «Математика»

Понятия: Формализация

Навигация: ← Глава 3. Композиция, цепное правило и формальное сердце E∘ L · Глава 5. Аналитический мост eval и теорема Таннери: замыкание уравнения логарифма →

src/CauchyProduct.v (19 Qed, 0 Admitted): mertens_cauchy_product — без новых аксиом, только L3 (разностное тождество mertens_diff_eq и конечный Fubini partial_sum_conv_swap аксиомо-свободны). Машинно проверено. ↩
src/ExpFunctionalEquation.v (17 Qed, 0 Admitted): exp_add (теорема сложения) через exp_conv_rec (рекуррентность $(n + 1) c_{n + 1} = (u + v) c_{n}$ ). Без новых аксиом, только L3. Машинно проверено. ↩
Там же: exp_limit_zero ( $exp 0 \sim 1$ ), exp_neg ( $exp (u) \cdot exp (- u) \sim 1$ ). Без новых аксиом, только L3. ↩
src/ProcessExp.v (21 Qed, 0 Admitted): ядро Qpow_diff_bound (липшиц степеней), exp_partial_lipschitz, exp_partial_tail_bound — аксиомо-свободны; сборка exp_meta_cauchy и сама exp_R — без новых аксиом, только L3. Машинно проверено. ↩
src/ProcessExp.v: exp_R_add (диагональный Мертенс), exp_R_zero, exp_R_neg, exp_R_wd (корректность на классах). Без новых аксиом, только L3. ↩
Там же: exp_R_inj через exp_R_inj_kernel ( $exp_{R} (D) \sim 1 \Rightarrow D \sim 0$ ) и монотонную оценку exp_lower_bound. Без новых аксиом, только L3. ↩
Проверено машинно: Print Assumptions для mertens_cauchy_product, exp_add, exp_R, exp_R_add, exp_R_zero, exp_R_neg, exp_R_inj даёт ровно одну аксиому — Classical_Prop.classic (L3); ни выбора, ни функциональной экстенсиональности. ↩

Путь Мудрости

Проводник

Глава 4. Процессная экспонента exp_ℝ

Замысел главы и смена яруса

Движок: теорема Мертенса

Рациональная экспонента: сложение и гомоморфизм групп

Экспонента процесса: $exp_{R}$ {exp_R}

Гомоморфизм и инъективность

Разбор E/R/R, ярус и что глава готовит

Вид графа

Оглавление

Обратные ссылки

Путь Мудрости

Проводник

Глава 4. Процессная экспонента exp_ℝ

Замысел главы и смена яруса

Движок: теорема Мертенса

Рациональная экспонента: сложение и гомоморфизм групп

Экспонента процесса: expR​{exp_R}

Гомоморфизм и инъективность

Разбор E/R/R, ярус и что глава готовит

Footnotes

Вид графа

Оглавление

Обратные ссылки

Экспонента процесса: $exp_{R}$ {exp_R}