Приветствую участников форума.
Хочу представить на обсуждение проект «Plexus» — попытку построения формального основания для дискретной геометрии и альтернативной алгебры без использования чисел с плавающей точкой (0 float в ядре системы).
Основные тезисы и результаты проекта:
1. Базовым объектом является диполь
с 4 состояниями:
(0,0),
(1,0),
(0,1) и
(1,1). Ключевое отличие от float: состояния «пусто» (
) и «конфликт» (
) различимы.
2. На этой основе строятся
-алгебра на шаре Пуанкаре, мёбиусовы гирогруппы, а также дискретные модели для квантовых вычислений (коды коррекции ошибок) и динамических систем.
3. В качестве примера прикладного применения исследуется стабилизация нелинейностей в уравнениях типа Навье–Стокса (насыщение при
за счет композиции законов вместо классического взрыва).
Вся теоретическая часть проекта полностью формализована и доказана в Lean 4 (ядро содержит 2197 теорем, mathlib и сторонние аксиомы не используются). Исполняемый рантайм и тесты (более 600 прогонов) написаны на Rust.
посмотрите по возможности подскажите, но сначала изучите не судите по обложке
Ссылка на публичный репозиторий:
https://github.com/toliktrast-sys/plexus
