Абсолютность AFN-T — пятиосевая абсолютность AFN-T

Статус

пятиосевая абсолютность AFN-T — пятиосевая абсолютность AFN-T: теорема справедлива равномерно по всем структурным осям вариации формальной математики.

Каноническое изложение — препринт MSFS §7, Theorem thm:five-axis.

Настоящий документ содержит Diakrisis-специфическую интерпретацию пяти осей и их связь с каноническим примитивом $(\langle\langle \cdot \rangle\rangle, \mathsf{M}, \alpha_\mathrm{math}, \sqsubset_\bullet)$.

Таблица пяти осей

Ось	Вариация	Diakrisis №	MSFS
Горизонтальная	$S \in \mathrm{R\text{-}S}$ (Rich-metatheories)	55.T	Theorem thm:horizontal
Вертикальная	$n \in \mathbb{N} \cup \{\infty\}$ (категорный уровень)	59.T.1	Theorem thm:vertical
Мета-вертикальная	$\mu$-iterations (meta-итерации)	69.T	Theorem thm:meta-vertical
Латеральная	$\xi$ (альтернативные categorical orderings)	84.T	Theorem thm:lateral
Полноты	$\pi$ (Ловер-scope)	87.T	Theorem thm:completeness

Комбинированное утверждение — MSFS Theorem thm:five-axis: для каждого кортежа $(S, n, \mu, \xi, \pi)$ AFN-T справедлива.

Логическая независимость осей

Важное уточнение (MSFS Remark rem:axes-dependence): пять осей не полностью логически независимы:

• completeness subsumes horizontal: каждая R-S лежит в Ловер-scope $\mathcal{L}\mathcal{S}$ по (R5).
• lateral ≡ vertical: альтернативные orderings редуцируются к $(\infty, n)$-Cat (Ara–Maltsiniotis, Барвик–Schommer-Pries).
• meta-vertical = $\mu$-closure of vertical: стабилизация на $(\infty, \infty)$ (Theorem thm:bergner-lurie-stab).

Минимальный логически независимый набор — 2 оси: горизонтальная + вертикальная. Пятиосевая формулировка сохраняется педагогически: каждая ось соответствует конкретному классу исторических обход-аргументов.

Diakrisis-интерпретация по осям

Горизонтальная — 55.T

Независимость AFN-T от выбора R-S. В Diakrisis-языке: для каждой $\alpha_S \in \langle\langle \cdot \rangle\rangle$ (артикуляции, соответствующей $S$), AFN-T справедлива.

Ключевая лемма (MSFS Lemma lem:SS-membership): формальная определимость $X$ в $F \subseteq S$ ⇒ $X \in \mathcal{S}_S$ (класс $S$-определимых объектов).

Связь с внутренней Diakrisis-структурой:

• $\alpha_\mathrm{math}$ не привилегирована (T-α): обобщается до любого $\alpha_S$.
• Gauge-группа $G$ автоэквивалентностей $\langle\langle \cdot \rangle\rangle$ транзитивно действует на R-S-индексированной фибрации $\rho$.

Вертикальная — 59.T.1, 66.T

Независимость AFN-T от категорного уровня $n$. Прямое доказательство на уровне $(\infty, \infty)$ (MSFS Theorem thm:direct-infty, соответствует Diakrisis 66.T «$(\infty,\infty)$-Ловер fixed-point») использует Ловер FP в $(\infty, \infty)$-cartesian closed category $\mathcal{C}_S := \colim_n \mathrm{Syn}^{(\infty,n)}(S)$.

Важное ограничение (MSFS Remark rem:direct-infty-scope): прямое доказательство на $(\infty, \infty)$ работает только для классических $S$ (Boolean internal logic). Для конструктивных $S$ (HoTT, MLTT, CIC, CZF) используется основная Theorem thm:afnt через Ламбек–Скотт reflection.

Diakrisis-аналог: для $\alpha_\mathrm{hott}, \alpha_\mathrm{cic}, \alpha_\mathrm{int}$ применяется T-α_c (конструктивный вариант).

Мета-вертикальная — 69.T

Замкнутость относительно meta-итераций $\mu$: $(\infty, \infty + 1)$-Cat $\simeq (\infty, \infty)$-Cat (Барвик–Schommer-Pries 2021 через $\Theta_n$ Резк 2010). Meta-иерархия не порождает структурной новизны за пределами $(\infty, \infty)$.

Diakrisis-аналог: iterated $\mathsf{M}^k(\alpha)$ не эскалирует до уровня 6 через мета-orbit.

Латеральная — 84.T

Альтернативные категорные порядки (operadic, globular, cubical, opetopic, double) редуцируются к $(\infty, n)$-Cat. Diakrisis-следствие: $\rho$-проекция инвариантна к выбору categorical ordering.

Полноты — 87.T (Ловер-scope)

Полная характеризация: любая foundational-theoretic вариация сводится к одной из четырёх осей в пределах Ловер-scope $\mathcal{L}\mathcal{S}$. Пятая ось $\pi$ закрывает вопрос «есть ли незамеченная ось?» формально.

Формальное определение $\mathcal{L}\mathcal{S}$ — MSFS Definition def:law-scope. Условия (L1)-(L4): syntactic category + semantic 2-category + адъюнкция $\mathrm{Syn} \dashv \mathrm{Mod}$ + $(\infty, n)$-realization.

Структурная связь с AFN-T

пятиосевая абсолютность AFN-T — это комбинированное утверждение: AFN-T + 5 осей = AFN-T (Absolute Foundation No-Go Theorem). Диаграмма зависимостей пяти осей в препринте — Figure fig:five-axis.

Следующие теоремы

После установления пятиосевая абсолютность AFN-T (пять осей) — три стандартных обход-paths должны быть формально закрыты (/06-limits/08-intensional-refinement, MSFS §8) и мета-классификация уровень 5+ должна быть стабилизирована (/06-limits/09-meta-classification, MSFS §9).

Ссылки

• MSFS §7 — основное изложение пяти осей;
• MSFS §10 — positioning против Эрнст 2015, Хэмкинс multiverse, BSP 2021;
• /10-reference/04-afn-t-correspondence — полная таблица номеров.