Глава 1. Граница финитизации на уровне функций

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

Часть XV довела до конца один сюжет: вычисление есть граница финитизации, ставшая алгоритмической. Та самая черта, что в Части IV делила рациональное и иррациональное, здесь прошла между разрешимым и неразрешимым: алгоритм над конечными данными либо завершается — и тогда он на Element-стороне, либо нет — и тогда он role-limit. Но всё это — граница на уровне чисел и алгоритмов над числами. Объект, который она делила, был числом: рациональное число, длина бега, код программы.

Эта часть поднимает ту же черту на ступень выше — на уровень функций. Утверждение части простое и параллельное прежнему:

функция, реифицированная как процесс, делится той же границей Element/role-limit: многочлен (конечная поддержка коэффициентов) есть Element, неполиномиальный формальный ряд (бесконечная поддержка) — role-limit относительно полиномиального слоя.

Трансцендентные функции — более сильный подслой этой role-limit-стороны: не всякий бесконечный ряд трансцендентен (геометрическая $1/(1-x)$ рациональна, но неполиномиальна). И как у чисел эта граница не была дефектом, а была устройством (иррациональное — не испорченное рациональное, а число-процесс, не сводящийся к конечной дроби), так и здесь неполиномиальный ряд — не «не дотянувший до многочлена» объект, а функция-процесс, чей коэффициентный хвост не обрывается.

Глава кладёт основание всей части. Она отвечает на три вопроса. Первый: почему в нашей системе числа уже суть процессы, а функции — ещё нет, и в чём эта асимметрия (§ 16.1.2). Второй: как её снять — как реифицировать функцию процессом (§ 16.1.3). Третий: где на функциях проходит граница Element/role-limit и чем многочлен отличается от неполиномиального ряда ровно так же, как рациональное от иррационального (§ 16.1.4). Затем — лестница объектов число $\to$ функция $\to$ функционал (§ 16.1.5) и разбор E/R/R с переходом к исчислению рядов (§ 16.1.6).

Дальше часть развернёт это основание: исчисление функций-процессов (Глава 16.2), их композицию и формальное сердце тождества $e^{-\ln (1-x)}=1/(1-x)$ (Глава 16.3), процессную экспоненту над вещественным аргументом-процессом (Глава 16.4) и аналитический мост, замыкающий функциональное уравнение логарифма (Глава 16.5). Завершит часть синтез лестницы реификации (Глава 16.6).

Онтологическая асимметрия: числа реифицированы, функции — нет

Вернёмся к тому, что было сделано с числом. В Части IV вещественное число перестало быть завершённой точкой прямой и стало процессом: RealProcess есть $N\to Q$ — последовательность рациональных приближений, на каждой стадии конечная, в пределе никогда не завершённая. Число есть этот процесс (точнее — класс эквивалентных процессов). Иррациональное число не дано как объект; оно разворачивается как способ бытия конечно-актуального (P4).

Теперь посмотрим, что в нашем построении происходит с функцией. И обнаружим асимметрию. Вся аналитика тома квантифицирует по $f$ как по внешнему отображению: $f:Q\to Q$ или $f:‘CauchySeq‘\to ‘CauchySeq‘$ — объект мета-уровня, Rocq-функция, которой теория пользуется, но которую как объект-в-теории не строит. Непрерывность, производная, интеграл — всё это свойства, навешенные на ambient-$f$ снаружи. Число реифицировано; функция — нет.

Это онтологическая неполнота. Система говорит: «процесс есть способ бытия конечно-актуального» — и проводит это для чисел до конца. Но её собственные функции этим способом бытия не обладают: они живут этажом выше, как мета-отображения, к процессной онтологии не сведённые. Пока это так, утверждение «всё в нашей математике — процесс» остаётся неполным: оно верно о числах и неверно о функциях.

И — это та же граница финитизации, что в Части IV, только об объекте другого уровня. На уровне чисел она различала рациональное (Element) и иррациональное (role-limit). На уровне функций ей естественно различать многочлен (Element) и неполиномиальный ряд (role-limit). Но чтобы граница могла пройти по функциям, функция сперва должна стать объектом, по которому есть что проводить, — то есть процессом. К этому и переходит следующий раздел.

Реификация: функция как коэффициент-процесс

Реификация повторяет ход Части IV ровно на ступень выше. Там число становилось процессом своих рациональных приближений. Здесь функция становится процессом своих коэффициентов.

Аналитическую функцию $f$ запишем рядом по степеням:

$$f(x)=\sum _{n=0}^{\infty }{c}_n{x}^n.$$

Функция есть последовательность своих коэффициентов Тейлора $c_0,c_1,c_2,\dots$ — то есть процесс $N\to Q$, ставящий каждому индексу $n$ его коэффициент. Это и есть реификация: формальный степенной ряд, носитель которого — коэффициент-процесс.¹

Definition FPS := nat -> Q.

Сходство с числом-процессом точное, и его стоит проговорить. RealProcess был $N\to Q$ — $n$-я стадия давала рациональное приближение к числу. FPS тоже есть $N\to Q$ — но $n$-я стадия даёт рациональный коэффициент функции. В обоих случаях: на каждой стадии — конечное рациональное данное (P4, Element-сторона), а сама функция — потенциально не обрывающийся процесс этих данных. Разница лишь в том, что индексирует процесс: у числа — точность приближения, у функции — степень при $x$.

В этом языке базовые функции анализа суть конкретные коэффициент-процессы:²

• геометрическая $\frac{1}{1-x}={\sum }_n{x}^n$ — процесс с постоянным коэффициентом $c_n=1$;
• экспонента $e^x={\sum }_n\frac{x^n}{n!}$ — процесс $c_n=1/n!$;
• логарифм $-\ln (1-x)={\sum }_{m\ge 1}\frac{x^m}{m}$ — процесс $c_0=0$, $c_m=1/m$.

Каждая из них — не завершённый объект, а правило, выдающее $n$-й коэффициент за конечное число шагов. Уже здесь стоит отметить различие, к которому глава вернётся: геометрическая $1/(1-x)$ — функция рациональная (её ряд бесконечен, но сама она — отношение многочленов), тогда как экспонента и логарифм — классические трансцендентные. Все три неполиномиальны; трансцендентность — более тонкий разрез внутри неполиномиального слоя. Функция стала тем же, чем в Части IV стало число: процессом.

Граница Element/role-limit на функциях

Реифицировав функцию, мы получаем объект, по которому граница финитизации может пройти. И она проходит ровно там, где у чисел: по тому, обрывается ли процесс.

Функция-процесс есть Element, если её коэффициент-процесс терминирует: начиная с некоторого индекса $N$ все коэффициенты равны нулю. Это в точности многочлен — конечная сумма степеней. В нашей системе это записано так:

Definition is_polynomial (f : FPS) : Prop :=
  exists N, forall n, (N <= n)%nat -> f n == 0.

Многочлен терминирует в том же смысле, в каком терминирует рациональное число и завершающийся алгоритм: после конечного объёма данных нового не возникает, хвост процесса — тождественный нуль. Постоянная функция, тождество, любой многочлен — на Element-стороне.³

Функция-процесс есть role-limit, если её коэффициент-процесс не терминирует: какой бы порог $N$ ни взять, дальше найдётся ненулевой коэффициент. Это в точности неполиномиальный формальный ряд: коэффициентный процесс не имеет нулевого хвоста (трансцендентность — свойство более сильное и с неполиномиальностью не совпадает: геометрическая неполиномиальна, но рациональна). И этот статус доказывается прямо: геометрическая и экспонента не являются многочленами.⁴ У геометрической все коэффициенты равны единице; у экспоненты — $1/n!$, и оба никогда не зануляются. Хвоста-нуля нет — процесс не обрывается — функция role-limit.

Стоит увидеть, насколько это та же самая граница, что в Части IV. Там число было Element тогда и только тогда, когда его процесс приближений стабилизировался на конечной дроби (рациональное); и role-limit, когда приближения шли без конца (иррациональное). Здесь функция есть Element тогда и только тогда, когда её процесс коэффициентов стабилизируется на нуле (многочлен); и role-limit, когда коэффициенты идут без конца (неполиномиальный ряд). Один разрез — обрывается процесс или нет, — применённый к объектам разного уровня.

И как иррациональное число не было дырой, а было процессом (Часть IV), так и неполиномиальная функция здесь — не недостроенный многочлен, а полноправный объект-процесс. Что это работающий объект, а не пустое имя, видно уже сейчас: определяющее уравнение геометрической функции $(1-x)\cdot \frac{1}{1-x}=1$ проверяется на уровне коэффициентов — свёртка процессов $(1,-1,0,\dots )$ и $(1,1,1,\dots )$ даёт $(1,0,0,\dots )$.⁵

Лестница реификации: число $\to$ функция $\to$ функционал

Сделанное в этой главе встаёт в общий ряд. Процессная программа тома идёт по лестнице объектов, и граница Element/role-limit проходит по каждой её ступени одинаково — по тому, обрывается процесс или нет.

уровень объекта	Element (терминирует)	role-limit (не обрывается)
число	рациональное	иррациональное
функция	многочлен	неполиномиальный ряд
функционал	(финитный)	(общий) — горизонт

Первая строка — Часть IV (и, в алгоритмической форме, Часть XV). Вторая — эта часть; и внутри её role-limit-слоя неполиномиальные ряды дальше различаются на рациональные, алгебраические и трансцендентные — более тонкая классификация, к которой часть ещё вернётся. Третья — горизонт: функционалы (отображения функций в числа или функции) ждут своей реификации так же, как функции ждали её до этой части; в нашей системе эта ступень пока не построена, и мы честно держим её как направление, а не как готовый этаж.

Важно, что это не три разные границы, а одна, поднимающаяся по уровням. Та же триада P4: на каждой ступени Element-сторона — конечно-актуальное, считаемое за конечное число шагов; role-limit- сторона — процесс, не сводящийся к завершённому объекту. Реификация функции — не отдельный трюк, а онтологическое завершение программы на следующей ступени: после чисел процессами становятся и функции.

Честно о статусе этого наблюдения. Различение многочлен / неполиномиальный ряд классично, и сами ряды — классический объект. Ново здесь не математическое содержание, а обрамление: функция, введённая как процесс-в-теории (а не как внешнее отображение), и прочтение границы как того же разреза Element/role-limit на ступень выше. Уровень результата — синтез и наблюдение (как у самой границы финитизации), не новая теорема. Но обрамление это работающее: на нём, как покажет часть, строится исчисление функций-процессов и замыкается конкретное тождество обратной функции.

Разбор E/R/R и что глава готовит

Соберём главу в триаду E/R/R — так, как она прочитывается в самом носителе функции-процесса.

компонент главы	роль в системе	слой E/R/R
коэффициенты $c_n\in Q$ (конечные данные на стадии $n$)	носители	Element (P4)
FPS — функция как процесс коэффициентов	роль-функция	Role
многочлен $\iff$ хвост коэффициентов $\equiv 0$	терминация	Rule (Element)
неполиномиальный ряд $\iff$ нет такого хвоста	не-терминация	Rule (role-limit)

Elements. Коэффициенты $c_n$ — рациональные числа, на каждой стадии $n$ конечно-актуальные. Это Element-сторона: данные, наличные за конечное число шагов.

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

Rules. Граница задаётся одним правилом о хвосте процесса: есть терминирующий нулевой хвост — функция Element (многочлен); нет — role-limit (неполиномиальный ряд). То же правило об обрыве процесса, что делило числа в Части IV, теперь работает на функциях.

Диагностика P4. Функция-как-коэффициент-процесс делится границей финитизации ровно как число-как-процесс приближений: Element $\iff$ процесс терминирует, role-limit $\iff$ не терминирует. Это та же граница, поднятая на уровень выше иерархии объектов (число $\to$ функция). Никакой новой аксиомы она не требует: всё построенное в главе — 0-аксиомно и машинно проверено.⁶

Что глава готовит. У нас есть носитель — функция как коэффициент-процесс — и граница на нём. Чтобы реифицированные функции жили, на этом носителе нужны операции: сложение, умножение (свёртка), производная — то есть исчисление. Его строит Глава 16.2: формальные степенные ряды образуют коммутативное кольцо, на котором определены производная и правила Лейбница и степени. А определяющее уравнение геометрической, мелькнувшее здесь ($(1-x)\cdot \frac{1}{1-x}=1$ на коэффициентах), окажется первым примером того, как тождества анализа становятся проверяемыми процесс-рекуррентностями.

---

---

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

Навигация: ← Глава 7. Синтез: одна диагональ, один дискриминант — Часть XV · Глава 2. Исчисление функций-процессов →

Footnotes

1. src/FormalPowerSeries.v (37 Qed, 0 Admitted, 0 аксиом): Definition FPS := nat -> Q. Реификация функции как процесса её коэффициентов; имя FPS — formal power series. ↩

2. Там же, src/FormalPowerSeries.v: geom_fps := fun _ => 1 (геометрическая $1/(1-x)$, все $c_n=1$); exp_fps := fun n => / Qfact n (экспонента, $c_n=1/n!$); log1m_fps ($-\ln (1-x)$, $c_0=0$, $c_{k+1}=1/(k+1)$). Машинно проверено, 0 аксиом. ↩

3. src/FormalPowerSeries.v: fps_one_polynomial (единица — многочлен), fps_X_polynomial (одночлен $x$ — многочлен). Машинно проверено, 0 аксиом. ↩

4. Там же: geom_not_polynomial ($1/(1-x)$ не многочлен — все $c_n=1\ne 0$) и exp_fps_not_polynomial ($e^x$ не многочлен — $1/n!\ne 0$ при любом $n$). Машинно проверено, 0 аксиом. ↩

5. src/FormalPowerSeries.v: geom_inverse_fps — $(1-X)\cdot ‘geom‘=‘1‘$ на коэффициентах. Машинно проверено, 0 аксиом. Это уже исчисление функций-процессов — к нему Глава 16.2. ↩

6. Весь носитель и граница главы — из src/FormalPowerSeries.v (37 Qed, 0 Admitted, 0 аксиом, Print Assumptions = «Closed under the global context» для ключевых лемм). ↩