Перенесённое правило состоит из ТРЁХ частей: самого правила, места вызова и текста отказа

Когда правило доказательства переносится со стороны на JavaScript на сторону на flang, переносить надо не две вещи, а три. Третья — прозаический текст отказа, и забыть её легче всего, потому что она не код и не влияет ни на один вердикт. Сверка двух ядер идёт ПОБАЙТОВО по всему, что уезжает в ведомость, а текст отказа туда уезжает. Поэтому новое правило двигает и те программы, которых оно никогда не доказывает.

Улика, на которой это видно чище всего. Программа «ПОДДЕЛКА: утверждение про СПИСОК инвариантом накопителя не доказывается» — нарочно дурная, её обязаны ОТВЕРГНУТЬ оба ядра, и оба отвергают её и до правки, и после. В списке расхождений она стояла ровно потому, что сторона на JavaScript дописала к отказу тождества две фразы (про перестановку соседей и про свёртку, растущую ровно на один), а сторона на flang их не имела. Перенеси я только две функции и место их вызова — семь утверждений закрылись бы, а эта программа осталась бы красной, и причину пришлось бы искать заново.

Чем подтверждено. Ветка work/zelenyy-stvol, основание 3c14d371, 19 августа 2026. Прогон node --test --test-name-pattern='ПОБАЙТОВО' flang/test/self-proofterm.test.mjs: до — совпало ПОБАЙТОВО 309, расхождений 15, после — совпало ПОБАЙТОВО 318, расхождений 6. Перенос — одинаковыДоПорядкаСоседей и свёрткаРовноНаОдин из flang/proof/reduce.mjs в flang/self/proof-kernel.flang.

Цена переноса, замером. 185 строк на flang против 155 строк на JavaScript — коэффициент 1,19, внутри полосы 1,1–1,5, снятой на четырёх прошлых переносах того же слоя. Из 185 строк на два новых правила ушло 10 функций, на текст отказа — одна строка, на место вызова — шесть.

Правило отвергает ложь, и это проверено отдельно. Четыре подделки, все четыре ядро отвергло словами «объявлено, не доказано»: начало свёртки не совпадает с основанием правой стороны; свёртка идёт по одному списку, а длина справа взята у другого; шаг прибавляет два; и — граница правила — перенос через скобки, то есть АССОЦИАТИВНОСТЬ, ложная в IEEE-754. Положительный контроль (перестановка двух соседей одного узла) закрылся правилом «тождество после переписки допущением». Список АКСИОМЫ остался пуст.

Чем ограничено. Утверждение верно для слоёв, где сверка двух реализаций сличает ТЕКСТ, а не только код отказа. Там, где сравнивают коды, третья часть не нужна — но тогда и сверка слабее: два ядра могут отвергнуть одно и то же по разным причинам, и автор чинил бы не то, что сломано.

Связано: equality-goals-hit-summand-order-not-missing-induction, byte-for-byte-comparison, a-removal-must-turn-a-test-red, line-numbers-in-a-task-verify-the-branch-it-was-written-against