Правый край сравнения сам по себе не закрыл ничего: закрыла ЛЕВАЯ сторона, прочитанная как мера списка

Заметка claims-about-length-are-two-thirds-of-what-the-kernel-refuses предложила порядок работ: «разрешить справа терм с известными границами — 36 отказов из 85; прочитать длина как меру списка — ещё 23. Первое дешевле и берёт больше». Первое взято отдельной веткой и закрыло НОЛЬ. Взяло всё второе.

Чем подтверждено. Правило «порядок по построению» (граница — ТЕРМ) приехало в ствол веткой work/length-remembers и делает ровно то, что предлагал прогноз: у цели Е не больше Г граница вправе быть выражением, а не литералом. Прогон node flang/scripts/proof-ledger.mjs и поштучный замер по flang/stdlib до и после: отвергнутых 91, стало 91. Ни одного. Изменилось только имя правила в отказе: 41 «у цели нет вида, к которому есть правило» → 12 «нет вида» плюс 29 «порядок по построению не проходит».

Почему прогноз разошёлся. 29 из 36 обещанных — это цели вида (длина результат) не больше (длина элементы), и после подстановки тела на место результат слева стоит не терм с границами, а форма тела: разбор (8 целей), свёртка (6), фильтр (3), пусть (3), вызов, выбор. Правый край у этих целей уже был в порядке — длина аргумента ядро читает и дно её знает. Не хватало ЛЕВОЙ стороны: чем является длина от того, что построила функция.

Что закрыло на самом деле. Пять случаев, дописанных тому же правилу 4, плюс та же переписка под правилом тождества — ветка work/pravyy-kray, коммиты 465d9474…6a6effd1:

Отказов 91 → 77 (закрыто 23 → 37). По всему корпусу ведомость: доказано ядром 170 → 187, сетка 124 → 107, и все семнадцать — без единой теоремы (82 → 99). Обратно не раскрылось ни одного.

Перемерено на стволе при слиянии (19 августа 2026). Числа выше сняты на основе ветки; ствол к часу слияния ушёл вперёд, и на нём та же работа даёт node flang/scripts/proof-ledger.mjs: доказано ядром 185 → 203, сетка 124 → 107, без теоремы 96 → 114. Направление и величина те же (плюс восемнадцать, минус семнадцать), «сетка 107» совпала знак в знак; расходится только точка отсчёта. Числа взяты прогоном на слитом дереве, а не со стороны.

Чем ограничено. Ни один из пяти случаев не «допускает» — каждый выводит. Правило по-прежнему заключает Е ≤ Г только когда обе стороны выведены, и посылка «не NaN» берётся тем же способом, что у правила 1: доказанная неотрицательность границы и есть свидетельство не-NaN. Утверждение «длина результата не больше длины входа» ядро НЕ принимает как таковое — оно проверяет это на теле, и на теле, которого не понимает, отказывает.

Мера читается только у форм, где она считается ТОЧНО. Список закрыт: выписанный целиком список, строка-литерал, выбор, разбор, отображение, добавить, приписать. отфильтровать и свёртка в него не входят ни строкой — у них есть только неравенство, и живёт оно там, где видно посылки.

Связано: claims-about-length-are-two-thirds-of-what-the-kernel-refuses, the-bottleneck-is-rule-strength, bottleneck-moved-to-claim-shape, what-blocks-the-kernel-now-is-induction-without-a-theorem