Доказательства FTS: теоремы, сертификаты и научные границы
Строгость начинается с точной формулировки утверждения. FTS может проверить, что конкретный факт найден по однозначному пути и что цепочка морфизмов типизируется.
теорема «Заказ ЗК-7781 можно отгрузить»
дано Заказ имеет «готов к отгрузке» равное да
в данных заказы найти где номер равен «ЗК-7781»
по морфизму «Готовый заказ можно отгрузить»
следовательно «Отгрузить заказ разрешено»
Symbolic proof
Без context FTS строит символическую деривацию: при условии существования заявленного witness и закона морфизма conclusion типизируется. Статус не должен выдаваться за доказательство факта реального мира.
Verified certificate
fts certify связывает теорему с конкретным JSON snapshot, канонизирует данные
и вычисляет digest. fts verify повторяет derivation и сравнивает сертификат.
Изменение evidence меняет digest и ломает проверку.
fts certify shipment.fts --context snapshot.json > certificate.json
fts verify shipment.fts --context snapshot.json --certificate certificate.json
Что доказано строго
При успешной проверке доказано относительно реализации verifier:
- документ прошёл синтаксическую и семантическую проверку;
- witness найден по указанному пути и равен ожидаемому значению;
- домен каждого морфизма совпал с текущим типом;
- conclusion совпал с результатом композиции;
- canonical evidence и certificate digest согласованы.
Что не доказано
- истинность внешнего бизнес-закона;
- полнота модели мира;
- отсутствие дефекта в реализации компилятора;
- актуальность snapshot в момент эффекта;
- юридическая новизна или патентоспособность идеи.
Путь к публикационному уровню
Для диссертационной работы нужен отдельный формальный слой: синтаксис и операционная семантика, typing judgments, формулировки preservation/progress или выбранных safety-свойств, доказательства, reference implementation и репликационный пакет benchmark. Для патента дополнительно нужен поиск prior art и работа с патентным специалистом до публичного раскрытия в тех юрисдикциях, где публикация разрушает новизну.
Сертификат FTS — хороший объект исследования и machine-checkable evidence, но не готовая патентная экспертиза.
Упражнение
Сформулируйте theorem, затем измените одно значение snapshot и одну букву в certificate. Обе подмены должны быть обнаружены. Отдельно выпишите assumptions, которые FTS принимает как внешние законы.
