Невысказываемое утверждение дороже недоказуемого

Найдено живым примером. Нужная лемма про «Фибоначчи шагом» оказалась непредставимой:

• утверждение «результат не меньше 0» о ней ЛОЖНО — накопитель объявлен число, и вход 0/−7/9 даёт −7;
• верна условная форма: «ЕСЛИ накопители неотрицательны, ТО результат неотрицателен»;
• записать её было нечем: слова требует в языке не было до 16 августа 2026.

Второй такой же случай — «Сколько дополнить» из flang/stdlib/strings.flang: правда держится на условии ветвления, а не на типах.

Почему это дороже недостающего правила. Правило можно добавить. Невысказанное утверждение не существует вовсе — его нет ни в списке доказанных, ни в списке недоказанных, оно невидимо для любой статистики охвата.

Следствие для замера цены. Считая, сколько функций доказано, надо делить неудачи на два разных исхода: «ядро не берёт» и «на языке не выразить». Иначе дыра в языке маскируется под слабость прувера.

Статус. Предусловие требует добавляется (ветка work/trebuet). Это же самое — импликация: «требует P, обеспечивает Q» есть P → Q.

Связано: the-bottleneck-is-rule-strength, condition-for-the-revolution