Ноль аксиом — проверяемое свойство, а не лозунг

Ядро flang ничего не принимает на веру. Прежняя редакция этой заметки говорила про пустой список АКСИОМЫ в flang/src/proofterm.mjs и про отдельный тест при нём — ни того, ни другого в дереве нет с 20 августа 2026: реализация на JavaScript удалена (fe8e8a37), сверки при ней — тоже (105943cd, 44 файла). Полгода ссылка вела в пустоту.

Держится свойство иначе, и это устройство важнее списка. Списка аксиом у ядра нет вовсе: аксиому туда нельзя «положить» — её можно только написать словами в исходнике. Поэтому проверка читает flang/self/proof-kernel.flang целиком и требует, чтобы слова «аксиома» в нём не стояло нигде, кроме названных доводов, объясняющих, почему то или иное правило — теорема, а не аксиома. Сверка идёт в обе стороны: довод из списка, которого в ядре нет, объявляется пропавшим.

flang io flang/scripts/kernel-forgeries.flang --plan 'Аксиом ноль'
→ аксиом ноль, нарушений 0   (код 0)

Каждое правило заводится с двумя обязательствами:

1. список случаев, который можно назвать целиком — не «правило умножения», а «умножение берётся, когда о каждом сомножителе известны обе границы отрезка»;
2. подделка, которая обязана быть отвергнута, и код отказа обязан её назвать.

Зачем такая строгость. Одна принятая на веру мелочь обесценивает всё остальное: доказательство, опирающееся на аксиому, стоит ровно столько, сколько стоит аксиома. Ноль аксиом — единственное состояние, при котором «доказано» значит «доказано».

Как это выглядит на практике. Правило про модуль числа заказывали как очевидное — и не завели, потому что заказанное утверждение оказалось ложным: nan-is-reachable. Правило про умножение завели только с посылкой об обеих границах, потому что «ноль умножить на бесконечность» даёт не число.

Связано: coq-strength-is-in-its-lemmas, the-core-proved-a-falsehood