Глоссарий Diakrisis

Обзор

Этот глоссарий — нормативный референс всех технических терминов Diakrisis. При расхождении с другими документами — глоссарий имеет приоритет.

Зачем нормативный глоссарий

• Единообразие: все документы используют одни и те же термины.
• Проверяемость: термины чётко определены.
• Обучение: один источник для справок.
• Предотвращение drift: термины не эволюционируют хаотично.

Формат

Каждая запись содержит:

• Символ / имя.
• Тип / статус.
• Определение.
• Место введения.

Опционально:

• Verum-статус (✓ / в разработке / не планируется).
• Связи с другими терминами.
• Примеры использования.

Основные символы

⟪⟫

Тип: 2-категория. Определение: локально-малая 2-категория с внутренней замкнутостью. Введено: Axi-1, /02-canonical-primitive/01-four-tuple. Verum: в разработке (базовая 2-категорная структура). Синонимы: метакатегория, пространство артикуляций.

𝖬

Тип: эндо-2-функтор ⟪⟫ → ⟪⟫. Определение: выделенный эндо-2-функтор — «метаизация». Введено: Axi-2. Verum: в разработке. Свойства: accessible (Axi-4), 2-функториальный.

α_math

Тип: Ob(⟪⟫). Определение: выделенный объект (линза). Введено: Axi-3. Verum: требует инстанциации. Замечание: не универсальна (T-α).

⊏_κ

Тип: двухместное отношение на Ob(⟪⟫), индексированное ординалом κ. Определение: α ⊏_κ β ⇔ ∃ f: α → 𝖬^κ(β). Введено: Def 10.3. Verum: в разработке (ordinal machinery). Свойства: рефлексивно (⊏_0), монотонно по κ.

α (с индексом)

Тип: Ob(⟪⟫). Определение: артикуляция (переменная). Использование: α, β, γ, ... для общих артикуляций; α_X для конкретных (α_zfc, α_hott, α_uhm).

ρ(α)

Тип: End(⟪⟫). Определение: ρ(α) := ev_{α_math}(α) = [α_math, α] — реализация α через α_math-линзу. Введено: Axi-4. Verum: в разработке (internal hom). Свойства: 2-функториальна, нетривиальна (Axi-5).

α_𝖬

Тип: Ob(⟪⟫). Определение: α_𝖬 := ι(𝖬) — представитель 𝖬. Введено: через Axi-1 + Axi-7. Verum: в разработке. Замечание: в Cat-модели Axi-8 нарушается; α_𝖬 Ёнеда-представим.

Fix(𝖬)

Тип: подкласс Ob(⟪⟫). Определение: {α : 𝖬(α) ≃ α} — класс неподвижных точек. Введено: 10.T5. Verum: в разработке. Свойства: непуст при accessibility 𝖬.

Ω̄

Тип: имя. Определение: обозначение для конкретной неподвижной точки ∈ Fix(𝖬). Использование: Ω̄_init (инициальная), Ω̄_term (терминальная).

Trace(𝖠)

Тип: подкласс Ob(⟪⟫). Определение: класс всех 𝖬^κ(α_0) для ординалов κ. Введено: Def 10.4. Verum: в разработке. Замечание: зависит от стартовой α_0.

A_init, A_fin

Тип: Ob(⟪⟫). Определение: инициальная 𝖬-алгебра и финальная 𝖬-коалгебра. Введено: 12.T1, 12.T2. Verum: в разработке (Адамек constructions). Свойства: существуют при accessibility.

Z (Z_1, Z_2, Z_3)

Тип: классы. Определение: три эквивалентные характеризации нулевой границы — путь, побег, граница представимости. Введено: Def (Z_i) + 16.T1. Verum: частично. Замечание: Z сама [И]; Z_i [О]/[Т].

𝓜_Fnd

Тип: moduli-пространство. Определение: Trace(𝖠)/gauge — классифицирующее пространство оснований. Введено: 43.T1. Verum: требует gauge-machinery. Свойства: содержит все Rich-основания как точки.

ι

Тип: 2-fully-faithful embedding. Определение: ι: End(⟪⟫) ↪ ⟪⟫ — вложение. Введено: Axi-1. Verum: в разработке.

Π, ♭, ♯

Тип: функторы когезивной структуры. Определение: Π (компоненты), ♭ (дискретизация), ♯ (ко-дискретизация). Цепочка: Π ⊣ ♭ ⊣ ♯ ⊣ ι. Введено: cohesion section.

G (gauge-group)

Тип: 2-группа. Определение: группа автоэквивалентностей ⟪⟫. Введено: gauge section. Свойства: действует на Trace(𝖠); 𝓜_Fnd = Trace/G.

𝒮_S — S-параметризованный класс структур

Тип: класс. Определение: 𝒮_S = класс всех мат-структур, определимых в Rich-метатеории S. Введено: уточнение Леммы 2' → 2ₗ/2ᵍ. Примеры:

• 𝒮_ZFC — все ZFC-определимые структуры.
• 𝒮_{NBG+AFA} — включает non-well-founded sets.
• 𝒮_HoTT — унивалентный types.
• 𝒮_linear — SMCC-структуры.

α_linear

Тип: Ob(⟪⟫). Определение: артикуляция Жирар-linear logic с exponential !. ν: ω+1. Classical-equivalence: через Жирар-трансляция.

α_affine

Тип: Ob(⟪⟫). Определение: аффинная логика без !-модальности. ν: ≤ ω. Замечание: не Rich (нет неограниченной индукции).

α_AFA-coalg

Тип: Ob(⟪⟫). Определение: финальная коалгебра 𝖬 в метатеории NBG + Ачел's AFA. ν: ω·2. Свойство: Morita-редуцируема к Ачел's M-types.

α_coinductive

Тип: Ob(⟪⟫). Определение: артикуляция coinductive types в теория типов (CIC, Agda). ν: ω+2. Связь: Morita-эквивалентна α_AFA-coalg.

𝒮_S^{local} и 𝒮_S^{global}

Тип: классы — локальная и глобальная части 𝒮_S. Определение:

• 𝒮_S^{local} — объекты, принадлежащие Ob(M_F) для некоторой модели M_F.
• 𝒮_S^{global} — объекты через natural transformations / sections of fibrations / derived constructions через family of models. Связь: 𝒮_S = 𝒮_S^{local} ∪ 𝒮_S^{global}. Роль: Лемма 2ₗ (локальная) + 2ᵍ (глобальная).

α_poly-HoTT

Тип: Ob(⟪⟫). Определение: артикуляция Homotopy Type Theory с cumulative universe polymorphism (Poly-HoTT). ν: ω·2+1. Структура: иерархия 𝒰_0 : 𝒰_1 : 𝒰_2 : ... + polymorphic terms ∏_ℓ Body(ℓ). Связь: реализована в Lean 4, Coq, Agda. Morita-редуцируема к derived category over universes. По 55.T/56.T: не уровень 6.

α_inf-cat

Тип: Ob(⟪⟫^{∞}). Определение: артикуляция в (∞,∞)-категорной Diakrisis. ν: Ω (class-ordinal). Структура: все (∞,n)-уровни нетривиальны; полная higher когерентность. По 59.T: не уровень 6. Детали: /06-limits/06-absoluteness.

(∞,n)-Cat

Тип: класс категорий. Определение: категории с k-морфизмами для k ≤ n; (n+k)-морфизмы обратимы для k ≥ 1. Иерархия: (∞,0) ⊂ (∞,1) ⊂ ... ⊂ (∞,∞). Стабилизация: (∞,∞) — максимальная осмысленная категорная сложность (59.T.2).

τ_{≤n} (n-усечение)

Тип: functor (∞,∞)-Cat → (∞,n)-Cat. Определение: локализация, слияющая k-морфизмы для k > n в identity. Свойства: теряет информацию при нетривиальных higher coherences. Значение: 2-Diakrisis = τ_{≤2}(∞-Diakrisis).

Особые объекты УГМ

Γ ∈ D(ℂ⁷)

Тип: плотностная матрица. Определение: positive semi-definite, trace 1 operator на ℂ⁷. Физ. смысл: состояние УГМ. Verum: требует quantum library.

ℒ_Ω = ℒ_0 + ℛ

Тип: Lindblad generator. Определение: ℒ_0 (standard Lindblad) + ℛ (regeneration). Эволюция: dΓ/dt = ℒ_Ω(Γ). Verum: в разработке.

ℒ_0

Тип: standard Lindblad generator. Определение: ℒ_0(Γ) = -i[H, Γ] + Σ_k L_k Γ L_k† - ½{L_k†L_k, Γ}.

ℛ

Тип: regeneration operator. Определение: действие, возвращающее Γ к ρ*. Уникально УГМ: не в standard NCG.

φ

Тип: self-модель (функтор). Определение: категорное отображение Γ → ρ*. Введено: T-96. Verum: требует category theory library.

ρ* = φ(Γ)

Тип: неподвижная точка. Определение: T-96 УГМ: ρ* = φ(Γ). Верно для: α_uhm ∈ Fix(𝖬).

α_uhm

Тип: артикуляция УГМ. Определение: специфическая α ∈ Trace(𝖠) с ν = ω·4. Структура: 7 инвариантов + динамика + self-модель.

P (purity)

Тип: мера на Γ. Определение: P = Tr(Γ²). Порог: P_crit = 2/7.

R (reflection)

Тип: мера рефлексии. Определение: R — мера «способности наблюдать себя». Порог: R_th = 1/3 (K=3 tripartite).

Φ (integration)

Тип: мера интеграции. Определение: аналог IIT Φ. Порог: Φ_th = 1 (T-129).

D (depth)

Тип: мера глубины. Определение: D — мера иерархической глубины. Порог: D_min = 2 (T-151).

SAD

Тип: self-awareness depth. Определение: SAD — мера self-awareness. Порог: SAD_MAX = 3 (C26).

Аксиомы (см. /10-reference/01-axioms-catalog)

• Axi-0..Axi-9.
• T-α.
• T-2f*.

Краткий перечень

• Axi-0: непустотность Ob(⟪⟫).
• Axi-1: структура ⟪⟫ (2-cat с internal closure).
• Axi-2: 𝖬 — 2-функтор.
• Axi-3: α_math ∈ Ob(⟪⟫).
• Axi-4: ρ через internal hom.
• Axi-5: ρ-нетривиальность.
• Axi-6: ρ и 𝖬 не перестановочны.
• Axi-7 (M-5w): самоартикулируемость.
• Axi-8 (M-5w*): критерий нетривиальности.
• Axi-9: достаточность.
• T-α: α_math не универсальна. Канонически — ∃ γ: γ ⊄_0 α_math (позитивный экзистенциальный). Классический эквивалент через двойное отрицание; конструктивный вариант T-α_c для интуиционистских gauge-классов.
• T-2f*: локально-стратифицированная комплетация.

Теоремы (см. /10-reference/02-theorems-catalog)

• 10.T1-T5, 11.T1-T3, 12.T1-T2, 13.T, 14.T1-T2, ...
• AFN-T.

Краткий перечень ключевых

• 10.T1: консистентность в Cat.
• 10.T2: Рассел-иммунитет.
• 10.T5: существование Ω̄.
• 13.T, 17.T: Escape теоремы.
• 16.T1: эквивалентность Z_i.
• 29.T: Универсальное основание.
• 30.T: Reconstruction.
• 43.T1: Classifying Space.
• AFN-T: no-go уровня 6.

Философские концепты

Διάκрисіс

Тип: акт, не объект. Определение: акт различения; феноменологический концепт. Введено: /01-diakrisis-phenomenon/00-act-not-object. Статус: [Ф] — феноменологический. Не формализуется: по AFN-T.

Нулевая граница

Тип: асимптотическая направленность. Определение: предел, к которому направлена трансфинитная 𝖬-башня. Соответствие: анаксимандровому apeiron, Z (формально). Статус: [И] — интерпретативный.

Акт / объект

Акт: процесс, событие, совершение. Объект: фиксированная сущность, установленное. Контраст: центральное различение Diakrisis.

Артикуляция

Тип: формальный аналог акта. Определение: след акта в формальной структуре. Представление: α ∈ ⟪⟫.

Gauge-класс

Тип: класс эквивалентности. Определение: артикуляции, связанные автоэквивалентностью. Примеры: [α_zfc] = [α_etcs].

Морита-эквивалентность

Тип: отношение эквивалентности. Определение: α_1 ∼_M α_2 ⟺ ρ(α_1) ≃ ρ(α_2). Связь: с gauge-классом в большинстве случаев.

Актика (ДЦ-дуал)

Актика

Тип: формальный ДЦ-дуал Diakrisis. Определение: 2-категория pointed reflective enactments, дуальная $\cF$ через adjoint pair $\varepsilon \dashv \alpha$. MSFS-соответствие: $\cE$ в Definition~\ref{def:enactments}. См.: /12-actic/00-foundations.

Энактмент

Тип: объект $\cE$ = $\rangle\!\rangle \cdot \langle\!\langle$. Определение (MSFS): квадрупл $(F, \cC, \iota, r)$ — теория + модель-категория + F-preserving pointing ι + выбранный reflector r (левый adjoint к ι) с тождествами треугольника. MSFS-соответствие: Definition~\ref{def:enactments}.

⟫·⟪

Тип: нотация Diakrisis. Определение: 2-категория актов/энактментов, дуальная ⟪⟫ через 108.T. MSFS-соответствие: $\cE$.

ε (AC-функтор)

Тип: 2-функтор $\langle\!\langle \cdot \rangle\!\rangle \to \rangle\!\rangle \cdot \langle\!\langle$. Определение: syntactic self-enactment, $F \mapsto (F, \Syn(F), \id, \id)$. Свойства: fully faithful, правый adjoint к α. MSFS-соответствие: $\varepsilon$ в Definition~\ref{def:enactments}.

α (OC-функтор)

Тип: 2-функтор $\rangle\!\rangle \cdot \langle\!\langle \to \langle\!\langle \cdot \rangle\!\rangle$. Определение: forgetful, $(F, \cC, \iota, r) \mapsto F$. Свойства: essentially surjective (после gauge), левый adjoint к ε. MSFS-соответствие: $\alpha$ в Definition~\ref{def:enactments}.

Reflector r

Тип: часть данных энактмента. Определение: левый adjoint $r : \cC \to \Syn(F)$ к $\iota$, с тождествами треугольника. Единственен up to unique invertible 2-cell (Рил–Верити 2022, Адамек–Росицкий 1994). Значение: обеспечивает canonicity essentially-surjective proof'а 108.T.

ε-инвариант

Тип: ординальный инвариант акта. Определение: активационная глубина акта — 7 уровней от 0 (событие) до Ω (апейрон-акт). Дуал: ν-инварианта артикуляции. См.: /12-actic/03-epsilon-invariant.

SSE ($\cS_S^\cE$)

Тип: $\cE$-аналог класса $\cS_S$. Определение (MSFS): componentwise closure базы $\SSE^{\mathrm{base}} = \{(F', \cM, \iota_\cM, r_\cM) : \cM \models S\}$ под операциями Definition~\ref{def:SS}. MSFS-соответствие: Definition~\ref{def:SSE}.

Dual Boundary Lemma / 109.T

Тип: дуал AFN-T. Определение: $\LAbs^{\cE} = \emptyset$ — не существует enactment-absolute. MSFS-соответствие: Theorem~ ef{thm:dual-afnt}. См.: /12-actic/05-dual-afn-t.

Ловер-scope на $\cE$

Тип: структурное условие для ε-completeness-axis. Определение: $\{(F, \cC, \iota, r) : F \in \mathrm{LS}(\cF) \wedge \cC \text{ closed symmetric monoidal}\}$ — включает Cartesian-closed, SMC, $*$-autonomous (универсальная диагональ Яновский). Покрытие: linear logic (Жирар), ludics, квантовые enactments, resource-sensitive type theories.

$\mathsf{A}$ (активация)

Тип: accessible endo-2-функтор на $\rangle\!\rangle \cdot \langle\!\langle$. Определение: дуал $\mathsf{M}$ — поднимает акт в практику более высокого порядка. Адъюнкция: $\mathsf{M} \dashv \mathsf{A}$ (124.T).

Метастемология (Е. Чурилов)

Тип: предшественник Актика в русской традиции. ε-координата: $\omega \cdot 2 + 1$ (125.T). Отличие: Чурилов позиционирует ДЦ как замещающий ОЦ (замещающий); Актика устанавливает формальную дуальность через 108.T.

Дополнительные $\mathcal{L}_\mathrm{Fnd}$-точки (MSFS-синхронизация)

Markov-конструктивизм (Марков+Нагорный)

Тип: $\mathcal{L}_\mathrm{Fnd}$-точка; конструктивная математика с принципом Маркова. Семантика: эффективный топос Хайланда; HA + MP; категорная реализация в $\mathrm{Eff}$. Положение: плюралистичный класс конструктивных оснований вместе с MLTT, BHK, реализуемостью. MSFS-референс: Table 2 (стр. 10), §3.2 Examples of R-S; MarkovNagornyj 1988.

Бишоп-конструктивизм

Тип: $\mathcal{L}_\mathrm{Fnd}$-точка; choice-free конструктивный действительный анализ. Семантика: любой топос с натурально-числовым объектом. MSFS-референс: Бишоп 1967, Bridges–Vita 2006.

Феферман-предикативизм

Тип: $\mathcal{L}_\mathrm{Fnd}$-точка; предикативная арифметическая сила $\mathsf{ATR}_0$. Свойство: предикативная комплекция. MSFS-референс: Феферман 1964.

Ультрафинитизм (Есенин-Вольпин)

Тип: граничный случай между $\mathcal{L}_\mathrm{Fnd}$ и Non-examples. Строгое прочтение: нарушает (R1) — полная индукция Пеано недоступна. Формализованные варианты: ограниченная арифметика $\mathsf{I}\Delta_0$, Buss $\mathsf{S}_2^i/\mathsf{T}_2^i$, $\mathsf{V}_0$, полиномиально-ограниченная арифметика — слабые Rich-метатеории; подстратум $\mathcal{L}_\mathrm{Fnd}^\mathrm{weak}$ (N-10 в gap-status). MSFS-референс: Есенин-Вольпин 1961, 1970; Buss 1986; Simpson 2009 (обратная математика); §3.4 Boundary cases.

Noesis (практическое расширение Diakrisis)

Тип: операционное расширение Diakrisis-корпуса; реализация мета-платформы знаний. Содержание: федеративная архитектура для индексации, навигации, сравнения и согласования мат-теорий на основе Diakrisis-формализма. Положение: не отдельный $\mathcal{L}_\mathrm{Cls}$-классификатор; наследует MSFS-координату Diakrisis через реализацию. Documentation: /noesis (раздел 11-noesis).

Родин А. — философское обоснование категорной множественности

Тип: философский lineage; не отдельная $\mathcal{L}_\mathrm{Fnd}$-точка. Содержание: прочтение категорных оснований как аксиоматической плюралистичности — consonant с формальной множественностью MSFS. MSFS-референс: Rodin 2014 (Axiomatic Method and Category Theory, Springer Synthese Library 364); Remark rem:soviet-tradition.

Методологические термины

П-0.0..П-0.7

Тип: методологические принципы. См.: /00-foundations/02-zero-principles.

Π_1..Π_5

Тип: тесты проверки. См.: /00-foundations/01-method.

К-1..К-5

Тип: критерии новизны. См.: AFN-T и .

К-Б-1..К-Б-5

Тип: критерии успеха Пути Б. См.: /09-applications/00-path-B-uhm-formalization.

S-1..S-5 / S'-1..S'-5

Тип: правила работы. S-серия: для Diakrisis в целом. S'-серия: для Пути Б.

NL-1..NL-14

Тип: негативные уроки. См.: /07-methodology/03-negative-lessons.

Статус-маркеры

• [Т]: теорема с полным доказательством.
• [Т-набр]: теорема с наброском.
• [Г]: гипотеза.
• [С]: условное (при допущениях).
• [П]: постулат.
• [О]: определение.
• [И]: интерпретация.
• [Ф]: феноменологическое.
• [✗]: ретрактировано.

Классы объектов

ℱ (формальные системы)

Rich-основания: ZFC, HoTT, CIC, MLTT, NCG, etc.

𝒮 (стандартные мат-структуры)

Множества, категории, топосы, (∞,n)-категории, etc.

C-8 (класс сборок)

Артикуляции с ν ≥ ω·2, выполняющие сложные критерии.

Следующий документ

/10-reference/01-axioms-catalog.