Дипольная алгебра V₄ и дискретная геометрия на шаре Пуанкаре

[Anatoliy79]

Приветствую участников форума.

Хочу представить на обсуждение проект «Plexus» — попытку построения формального основания для дискретной геометрии и альтернативной алгебры без использования чисел с плавающей точкой (0 float в ядре системы).

Основные тезисы и результаты проекта:
1. Базовым объектом является диполь $V_4$ с 4 состояниями: $VAC$ (0,0), $ACT$ (1,0), $INV$ (0,1) и $RES$ (1,1). Ключевое отличие от float: состояния «пусто» ($VAC$) и «конфликт» ($RES$) различимы.
2. На этой основе строятся $X$-алгебра на шаре Пуанкаре, мёбиусовы гирогруппы, а также дискретные модели для квантовых вычислений (коды коррекции ошибок) и динамических систем.
3. В качестве примера прикладного применения исследуется стабилизация нелинейностей в уравнениях типа Навье–Стокса (насыщение при $\omega=1$ за счет композиции законов вместо классического взрыва).

Вся теоретическая часть проекта полностью формализована и доказана в Lean 4 (ядро содержит 2197 теорем, mathlib и сторонние аксиомы не используются). Исполняемый рантайм и тесты (более 600 прогонов) написаны на Rust.

посмотрите по возможности подскажите, но сначала изучите не судите по обложке

Ссылка на публичный репозиторий: https://github.com/toliktrast-sys/plexus

[dgwuqtj]

Anatoliy79
Вы знаете, что такое числа с плавающей запятой? Конкретно о чём стандарт IEEE 754. К основаниям это не относится.