Проверка замкнутости цели стояла только на ветви индукции, и прямой шаг «по примеру» шёл мимо неё

Правило по примеру закрывает цель одним посчитанным значением. Это законно ровно тогда, когда значение у цели одно. Ядро это знало и проверяло — но проверка стояла на ОДНОЙ из двух дорог к правилу.

Внутри индукция по шаг шёл через «По примеру при заключении», где список свободных имён посылки обязан быть пуст. Шаг по примеру, написанный прямо под утверждаем, шёл другой дорогой — «По примеру при посылке» → «Прогнать пример» — и проверки не проходил вовсе. Итог: ядро печатало «доказано: терм принят ядром, 1 шаг — утверждение обо ВСЕХ входах» о постусловии, которое flang run нарушал на первом же входе.

Чем подтверждено. Ветка u/dyra-kvantor на d8bc4306, двоичный собран из семени дерева. flang/test/fixtures/poddelka-primer-pod-kvantorom.flang: check --proof → «доказано … обо ВСЕХ входах», run --function «Пятёрка» → FLANG_PROPERTY: нарушено свойство «всегда четыре». Те же два ответа на benchmarks/proof-cost/probe-forgery.flang (там утверждение ложно — Противоположное(−5) = 5 > 0, проверено вычислением) и на docs/benchmark/05-opposite.flang (там утверждение ИСТИННО, но одним примером не доказано; проверено вычислением на семи значениях).

Чем починено. Прямой шаг ведёт через ту же подстановку, какой пользуются по предположению и по свойству («Цель с телом»: тело функции встаёт на место результат), и дальше через ту же функцию «Свободные имена». Второй проверки не заведено — заведён второй вход в существующую.

Почему считать свободные имена по САМОЙ цели нельзя. В цели стоит результат, и он свободен и у замкнутой цели тоже. Отличить «результат зависит от входа» от «результат один на всю функцию» умеет только подстановка тела: у функции без параметров тело замкнуто, у функции с параметрами в подставленной цели остаются ровно те имена, от которых её значение зависит.

Сколько это стоило честных доказательств: ноль. Замер по всему дереву (951 файл, check --proof --json каждым из двух двоичных, сверка по тройке файл-функция-утверждение): вердиктов 1038 до и 1118 после, «доказано» 449 → 469. Слово «доказано» потеряли РОВНО ТРИ утверждения, и все три — названные выше улики. Прямых шагов по примеру в дереве 53; отвергнуты 3, остальные 50 (все на функциях без параметров — таблицы в flang/proof/examples/corpus-*.flang и три теоремы о границах точных чисел в flang/self/types.flang) остались доказанными.

Чем ограничено. Проверка отвергает и тот случай, когда подстановка тела захватила бы связанное имя: замкнутость такой цели ядро не решает и примером её не закрывает. В дереве таких целей нет ни одной, но правило строже необходимого именно здесь — нарочно.

Связано: the-core-accepts-falsehood-a-class, the-core-proved-a-falsehood, zero-axioms, bootstrap-seed-lags-the-sources-by-one-language-form