TMI-OS Experiment

Голый независимый экспериментальный домен для частых проверок и push.

LLM/GPT/Codex -> Lean -> TLFL -> И1

Назначение:

Intent -> CanonicalRecord -> Passport -> GuardedAction

Главный вход:

PASSPORT.md

Что это

Это не основное ядро TLFL и не публикационный архив. Это отдельная экспериментальная рабочая плоскость, где можно быстро проверять маленькие программы, формулы, доски и guard-правила до переноса в основной слой.

Что внутри

• catalog/ - каталог доменных пространств эксперимента.
• PASSPORT.md - главный паспорт, из которого компилируется домен.
• SYNC_STATUS.md - текущий читаемый статус синхрона и proof-оси.
• codex/PASSPORT.md - рабочий паспорт инструментальной роли Codex в эксперименте.
• control/DICTIONARY.md - контрольный словарь паспорта, без заглубления языка.
• docs/DEPLOY_FROM_PASSPORT.md - инструкция развертывания от паспорта через Lean / Vampire / E.
• examples/hello.i1 - минимальная программа на И1.
• experiment/index.html - локальная визуальная плоскость без зависимостей.
• spaces/installer_sandbox/ - маленькая песочница для проверки инсталлятора.
• spaces/bare_stack_clean_build/ - чистая локальная сборка Lean / Vampire / E.
• docs/BOUNDARY.md - граница: что можно держать здесь, а что нельзя.
• docs/BARE_STACK_BUILD.md - сборка голого стека Lean / Z3 / Vampire / E.
• scripts/check_experiment.sh - быстрый локальный guard-check.

Запуск

Проверить эксперимент:

./scripts/check_experiment.sh

Проверить маленькую песочницу инсталлятора:

./spaces/installer_sandbox/scripts/check_installer_sandbox.sh

Развернуть полный проверочный стек:

docs/BARE_STACK_BUILD.md

Запустить доменную clean build:

./spaces/bare_stack_clean_build/scripts/clean_build.sh

Открыть web-плоскость:

cd experiment
python3 -m http.server 8766

Затем открыть:

http://127.0.0.1:8766/

Правило

Эксперимент принимает идеи.
Эксперимент не публикует claims.
Эксперимент не хранит секреты.
Эксперимент не заменяет TLFL.