Слой доказательства: высказать утверждение и проверить доказательство

Чего не было

До этого слоя утверждение о поведении в языке высказать было нечем.

Постусловие в AST было и работало: его проверял интерпретатор (кадр post в flang/src/interpret.mjs) и печатали все восемь целей. Но кладёт его туда flang/src/compat.mjs — из свойство утилиты наследия FTS, — и flang/src/defunc.mjs — из сторожа объявленной меры. Поверхности у постусловия не было вовсе: обычная функция flang сказать о себе не могла ничего.

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

Кванторов не было. требует не было. обеспечивает не было.

Законы моноида, монады, изоморфизма и отношений множеств проверялись — и проверяются — конечной сеткой примеров автора: предел 12 значений, у монады 6, у стрелок 4. Это не доказательство и никогда им не было; ведомость доказательства (flang check --proof) для этого и появилась.

Что теперь есть

Три слоя, и границы между ними жёсткие. Индукция не завела четвёртого: принцип порождается (flang/proof/initial.mjs) и сводится (flang/proof/reduce.mjs) ВНУТРИ третьего слоя, а поверхность и обязательства о ней не знают ничего. Новых слов у поверхности от индукции ноль — она работает восемью уже стоящими, и это не экономия: девятое слово пришлось бы завести в таблице ключевых слов самоприменённого лексера, то есть увеличить ровно тот долг, в который эта работа и так упёрлась.

1. Поверхность: девять слов

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

Поверхность — Isar из Isabelle, и это сказано вслух намеренно. Isar придуман ровно ради читаемости структурированного доказательства, и переизобретать то, что уже себя доказало, не за чем: утверждаем — это show, дано — assume, затем — also/moreover, по свойству «…» — by (rule …), следовательно доказано — qed.

Тактик нет и не будет. Тактика — метапрограмма, ворочающая состояние цели поиском, а поиск нетотален по природе. В flang всё либо тотально, либо объявлено обычным, значит тактику на самом языке не написать — она жила бы только в эталоне на JavaScript. Такая дыра у нас была одна (убывает не имел продукции в самоприменённом парсере); её закрыли, и она осталась примером того, чего не заводят второй раз. Сегодня продукция убывает стоит в flang/self/parser.flang и стережётся отдельной строкой flang/test/self-parser.test.mjs:326, а весь список пробелов снимается с таблицы лексера прогоном и содержит одну запись — в монаде.

Цена решения нулевая: что бы тактика ни выдала, ядро всё равно проверяет ТЕРМ, поэтому тактики не входят в контур доверия и добавляются когда угодно позже.

Две формы под одним словом

Слово теорема несёт старую форму (наследие FTS) и новую. Различает их не слово, а содержимое блока, и решение принимается ПОСЛЕ разбора блока:

следовательно доказано не отнимает у старой формы её следовательно «вывод» потому, что склейка ключевых слов жадная и длиннейшая-первой — тот же довод, по которому закон и по закону мирно стоят рядом.

Смешение форм — отказ, а не склейка: у конструкции стало бы два смысла и ни одного объявленного.

Все теоремы наследия в дереве разбираются в тот же узел ftsLegacy, что и до этой работы. Это проверено на самих файлах репозитория (flang/test/proof-surface.test.mjs), а не на выдуманном примере.

Слова поверхности: занятость измерена, а не обещана

У всех девяти слов ноль голых вхождений в 153 файлах .flang и .fts корпуса. Измерено не глазами и не grep-ом, а flang/scripts/word-occupancy.mjs: он читает корпус тем же tokenize, каким его читает язык, и считает только токены name с quoted: false. Закавыченное имя ключевым словом стать не может никогда, поэтому «ёлочки», строки и комментарии не считаются — этим счёт и отличается от grep, который их считает и потому всегда завышен. Скрипт можно запустить и повторить число.

Четыре слова из восьми — фразы из двух слов, и не ради красоты речи: одинокое свойство уже занято (property), одинокое пример — тоже (example), а по — это by. Фразой из двух слов переменную не назвать никогда; тем же доводом в языке уже стоят порог отказов, код символа и обратный элемент.

Слова стоят на двух поверхностях из четырёх — русской и английской. На эсперанто и по-китайски таблица молчит, и это решение владельца языка, а не пропуск: по свойству, по примеру, по предположению и следовательно доказано — обороты этого языка, а не термины математики, и переводить придуманное значило бы выдумывать дважды. Тот же довод держит на двух поверхностях decreases («убывает»). Молчание измерено (flang/test/proof-surface.test.mjs), чтобы столбец нельзя было дописать за владельца молча. Пока его нет, доказательство пишется на двух поверхностях.

Девятое слово: требует — предусловие

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

Прочтение выбрано другое, и оно то же, что в Dafny: предусловие снимает вызывающий.

Три правила снятия, и все три уже были у ядра. Аргументы подставляются в предусловие вызываемого — получается инстанция. Дальше: сведением (те же два правила flang/proof/reduce.mjs при фактах вызывающего — его собственных предусловиях), вычислением (инстанция замкнута — то же правило, каким закрывается база индукции) и никак, с отказом, называющим вызов, предусловие и что было известно. Новых правил ноль, аксиом по-прежнему ноль.

Что это дало доказательству. Ближайшая названная граница ядра сдвинулась: посылка индукции, у которой связано свободное имя, раньше не закрывалась ничем — примером нельзя (значений бесконечно много), предположением индукции нельзя (частей нет). Предусловие её закрывает; так доказана «Высота от дна» в flang/proof/examples/precondition.flang. Появилось и доказательство вне индукции: цель с подставленным телом функции сводится к предусловиям, и это работает там, где объявленной суммы нет вовсе.

Чего у предусловия нет. Нет результат: результата до вызова не существует. Нет для всех: квантор при постусловии называет параметр для индукции, а предусловие снимается у каждого вызова по отдельности. Нет условия ветвления вызывающего как факта: собирать путевые условия значило бы завести анализ, которого у языка нет ни одного, — и это названо в отказе, а не скрыто. Роль гипотезы в теореме по-прежнему несёт дано; требует несёт гипотезу в функции, и это разные места.

Предусловие обязано говорить о входе. Замкнутое предусловие отвергается типизатором (FLANG_PRECONDITION): оно либо истинно всегда — и тогда обязывает вызывающих ни к чему, — либо ложно всегда, и тогда телу досталась бы допущением ложь, из которой выводится что угодно. Граница проверки названа: требует «ложь» н больше н упоминает параметр и всё равно невыполнимо; решателя у языка нет. Ложь при этом не выходит наружу — снять такое условие не сможет ни один вызывающий, и на границе оно тоже не пройдёт.

2. Обязательства (flang/src/obligations.mjs)

Постусловие написано у функции, теорема — отдельным объявлением, связаны они только именем. Ядру нельзя дать ни то, ни другое по отдельности: терм проверяется ОТНОСИТЕЛЬНО цели, а цель написана у функции. Значит между ними стоит слой, который сводит их в один объект — обязательство (verification condition).

Обязательство — это ДАННЫЕ, а не текст: цель, квантор, гипотезы, связка результата, размер сетки примеров и предложенный терм. Ни одной строки для человека, кроме id. Передавать ядру текст значило бы третий разбор одного и того же после лексера и парсера.

Три источника: постусловие, объявленная мера, теорема. Теорема не создаёт обязательство, а закрывает его. Теорема, которая ничего не закрывает, — отказ: доказано было бы неизвестно что.

Обязательство меры приходит уже закрытым, и закрыл его не автор: убывание доказал анализ завершаемости обходом графа вызовов до всякого доказательства. Ядру там делать нечего, и притворяться, будто есть, значило бы поставить в цепочку доверия шаг, которого нет.

Отказы этого слоя: теорема без цели, теорема не о том, что обещает функция (сличение синтаксическое — ядро не решает, что два разных утверждения означают одно и то же), два постусловия на одно имя, две теоремы на одно постусловие, переменная теоремы не параметр функции, незакрытое доказательство.

3. Ядро (flang/src/proofterm.mjs)

Ядро ничего не ищет. Ни перебора правил, ни подбора подстановки, ни решателя. Это не экономия: поиск и есть то, из-за чего проверяльщику нельзя доверять, не прочитав его целиком, а прочитать целиком можно только маленький. Шаг без названного факта отвергается с указанием, что назвать.

Индукция не заведена отдельным понятием. Индуктивный тип есть начальная алгебра, и её универсальное свойство даёт сразу и свёртку (она в языке с самого начала — свёртка … начиная с …), и принцип индукции. Поэтому принцип здесь читается с объявления суммы: случаев ровно столько, сколько конструкторов, и в рекурсивном случае доступно предположение о части значения. Ядро сличает случаи с объявлением — точным равенством множеств, а не покрытием: исчерпывающность разбор считает типизатор по тем же образцам, и разреши здесь лишний случай, два слоя стали бы отвечать на один вопрос по-разному.

3а. Принцип индукции — ТЕРМ, а не правило (flang/proof/initial.mjs)

Принцип не вписан в ядро ни для списка, ни для дерева, ни для перечисления. Он порождается по объявлению суммы и порождается как ДАННЫЕ, которые ядро потом сворачивает тем же «слабейшее побеждает», каким сворачивает всё остальное. Разница не стилистическая: правило на JavaScript пришлось бы читать целиком, чтобы ему поверить, а терм ядро проверяет.

Сигнатура функтора читается с объявления буквально:

тип «Дерево чисел»
  вариант «Пустое»
  вариант «Развилка» содержит значение: число, меньшие: «Дерево чисел», большие: «Дерево чисел»

F(X) = 1 + (число × X × X)

Сумма по вариантам, произведение по полям, X на месте каждого поля, чей тип — сам объявляемый тип. Выбирать не из чего: это то же объявление, переписанное другими знаками. Отсюда принцип:

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

Посылка без допущений называется базой, с допущениями — шагом. Это не два правила: у базы X встретился в посылке ноль раз, у шага — больше нуля. Поэтому перечисление («Светофор») доказывается тем же самым принципом, что дерево, а не «конечным исчерпанием как особым случаем». Проверено тем, что вердикт светофора теперь говорит «база 3 случая, шаг при допущении на частях (0 случаев)».

**Граница поля X названа прямо:** меньшие: «Дерево чисел» — место X, а дети: список «Дерево чисел» — нет, потому что за списком стоит другой функтор, и допущение о его элементах — другое допущение. Это та же граница, что у монады (monad.mjs: параметр обязан стоять в поле ЦЕЛИКОМ).

3а-бис. Второе объявление: у ВСТРОЕННОГО списка тоже есть начальная алгебра

Объявление, с которого читается принцип, бывает двух видов, и оба читаются. Первое пишет автор словами тип … вариант …. Второе не пишет никто — и оно всё равно есть: у встроенного список Э объявления в ПРОГРАММЕ нет, но есть в самом ЯЗЫКЕ, и лежит оно в трёх местах, каждое из которых язык уже считает сегодня.

Третий факт — тот самый, на котором стоит обещание «тотальная, структурой» у 212 функций корпуса. То есть допущение индукции о хвосте законно ровно постольку, поскольку законно это обещание: довод один и тот же, и второго здесь не заведено.

Это порождение, а не постулат. Аксиома — утверждение, принятое без доказательства, и её нельзя проверить; здесь же не утверждается ничего нового — три действующих факта переписаны в ту же форму, в какой автор пишет объявленную сумму (initial.mjs, объявлениеСписка). Список АКСИОМЫ остался пуст. Дальше ядро не различает, откуда объявление пришло: сигнатура функтора, посылки, точное покрытие и свёртка принципа у них общие, и правило «место X» — одно: поле, чей тип есть сам объявляемый тип. Способа узнать «тот же тип» два только потому, что типы записаны двумя способами: у суммы — именем (хвост: «Стопка»), у списка — целиком (хвост: список Э).

Строке алгебра НЕ дана, и это решение, а не пропуск. Тот же типизатор исчерпывает разбор строки теми же двумя образцами. Но функтор у неё другой: голова строки — тоже строка, значит по правилу «поле того же типа» местом X оказались бы ОБА поля, и принцип потребовал бы два допущения вместо одного. Это отдельная работа с отдельным доводом; сделать её заодно значило бы протащить непрочитанное решение под видом прочитанного. Отказ проверяется тестом, 19 функций strings.flang ждут очереди.

3б. Шаг индукции: чем он выведен (flang/proof/reduce.mjs)

по предположению больше не «объявляет допущение известным». Оно обязано свести заключение посылки к допущениям, и пока сведение не прошло — шаг не выведен. Правил сведения три, список закрыт, и все три печатаются в отказе поимённо:

Разница между первой и второй строкой — не описка и не пробел: сумма стоит в первом правиле и не стоит во втором, и ровно в этом состоит различие между дном и потолком отрезка нат.

И ЧЕТВЁРТЫЙ ХОД, КОТОРЫЙ НЕ ЯВЛЯЕТСЯ ЧЕТВЁРТЫМ ПРАВИЛОМ (раздел 3б-квинт): цель, в которой не осталось ни одного свободного имени, вычисляется. Спрашивается он ПОСЛЕ всех трёх и только при их отказе.

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

Останов виден глазами: каждая переписка либо уменьшает дерево, либо подставляет уже нормализованное поддерево. У четвёртой останов держится иначе, и об этом сказано прямо ниже: у неё есть названный предел, и это единственное место ядра, где счёт ведётся числом.

3б-бис. Четвёртая переписка: развёртка определения

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

Ограничение стоило двух утверждений корпуса, и обе улики измерены прогоном, а не вспомнены:

• «высота копии равна высоте оригинала» (flang/proof/examples/stack.flang) — шаг требует знать, чему равна «Высота» НА КОНСТРУКТОРЕ, и без этого стороны равенства остаются разными термами. Улика записана владельцем языка словами ровно так же;
• «глубина дерева неотрицательна» (flang/stdlib/tree.flang) — шаг упирается в «Глубже» от двух допущений, и о результате чужой функции ядро не знало ничего, хотя тело её написано тремя строками ниже. Улика стояла исполняемым заказом в flang/test/corpus-claims.test.mjs.

Развёртка — не пятое правило, а переписка, и это не формальность. Решающих правил по-прежнему два, и оба утверждения выше закрыты СТАРЫМИ правилами: первое — «тождеством после переписки допущением», второе — «неотрицательностью по построению». Развёртка не добавляет знания. «Ф» от а и тело «Ф» с подставленным а — одно выражение, записанное дважды: так определил автор, и типизатор эту подпись уже проверил. Ядро читает написанное — ровно так же, как читает ветвь разбор по известному конструктору. **Список АКСИОМЫ не пополнился ни на строку.**

Бесконечная развёртка рекурсии — главная опасность этой переписки, и потому у неё четыре ограничителя. Каждый назван, каждый стоит отдельной строкой в flang/proof/reduce.mjs, и у каждого свой тест-изъятие в flang/test/proof-kernel.test.mjs:

Ограничитель 4 знает ЧЕТЫРЕ связывателя, и до 16 августа знал три. Список назван в нём прямо, а не выведен, и в этом его цена: подставить в initial.mjs и нормализация в самом reduce.mjs научились отобразить/отфильтровать четвёртым связывателем, а сторож захвата остался с прежними тремя — и его собственная строка это утверждала («связывателей в языке три»). Дыра измерена программой, а не рассуждением:

тотальная функция «Сколько равных»
  принимает х: число
  длина (отфильтровать [1, 2, 3] где эл → эл равно х)

тотальная функция «Проверка»
  принимает эл: число
  для всех эл обеспечивает «равно трём»
    результат равно (длина (отфильтровать [1, 2, 3] где эл → эл равно эл))
  «Сколько равных» от эл

Развёртка подставляла эл вызывающей функции ПОД эл фильтра, цель сходилась правилом тождества знак в знак, и ведомость печатала «доказано сведением цели с телом функции … обо ВСЕХ входах». flang run на том же файле отвечал FLANG_PROPERTY на эл = 2: слева считается 0 или 1, справа всегда 3. Улика стоит негативным тестом (flang/test/proof-soundness.test.mjs, «ПОДДЕЛКА ЗАХВАТОМ»), рядом с ней — граница с другой стороны (тот же вызов с аргументом, названным иначе, разворачивается и доказывается по-прежнему), и изъятие красит именно её.

Появись пятый связыватель — его придётся вписать в ТРИ места сразу (подставить, шаг, связывает), и это записано здесь, потому что вывести список неоткуда.

Почему предел не может соврать. Развёртка только читает определение, поэтому остановиться раньше — значит доказать МЕНЬШЕ, а не доказать ложное. Ровно поэтому число 32 не входит в контур доверия: от него зависит, докуда доходит честная развёртка, и не зависит ни одно «доказано».

Ядро по-прежнему ничего не ищет. Определения приезжают в свести четвёртым аргументом — данными, наравне с допущениями и объявлениями. Не дали — развёртки нет вовсе, и нормализация та же самая, что была до этой работы; это отдельная проверка («развёртки нет, пока определений не дали»). Так же и в обратную сторону: initial.mjs нормализует тело функции ради ветвей разбор и определений не даёт нарочно — ветви разбора обязаны читаться с того тела, которое написано.

Что развёртка НЕ берёт, и это её граница, а не недоделка. «Копия» от х при неизвестном х не разворачивается: аргумент — имя, разбор по нему ветви не выберет. «Фибоначчи шагом» от н и 0 и 1 не разворачивается: рекурсия идёт по ЧИСЛУ, конструкторов у нат нет, а тело не плоское — в нём стоит вызов себя же. Именно поэтому допущения индукции никуда не делись: они и есть то, что известно о вызове, который разворачивать нельзя.

3б-кватер. Сужение по условию если: почему его у ядра НЕТ

Оба правила границ спускаются в если и требуют своего от обеих ветвей, а само условие не читают. Выглядит это упущением, и заказ на него стоял исполняемой строкой: flang/stdlib/numbers.flang «Абсолютное значение» написана как если число меньше 0 то 0 минус число иначе число, и «модуль числа неотрицателен» человеку очевидно. Приём в дереве есть и работает — сузить в flang/src/types.mjs (числовые отрезки) и там же сужение по пусто (непустота списка).

Приёма в ядре нет, и решение это измерено, а не выбрано. Замеры стоят исполняемыми в flang/test/proof-kernel.test.mjs («сужение по условию: цена измерена»), и их три:

NaN здесь не мысленный эксперимент: литерала для него у языка нет, но 0 делить на 0 проходит типизацию без единой диагностики — деление на ноль в flang даёт значение IEEE-754, а не отказ (builtins.mjs). В проверке вход именно посчитан программой, а не подан аргументом.

Отсюда же ответ про **остаток от**, которого нет ни в одном правиле. Посылок у него не одна, а две (для дна) и три (для потолка), и все три сняты прогоном (flang/test/stdlib-claims.test.mjs, «границы остаток от сняты прогоном»):

• знак остатка — знак делимого (-5 остаток от 3 = −2), значит нужна неотрицательность делимого;
• и его КОНЕЧНОСТЬ: бесконечность не меньше 0 истинно, а бесконечность остаток от 3 — не число. Одного дна правилу мало;
• для потолка м−1 нужна вдобавок целость: 2.5 остаток от 3 = 2.5, то есть больше, чем м−1 = 2.

Первые две посылки у ядра появились — это вОтрезке из работы над умножением (ветка work/kernel-mul-field), — и правило пишется одним истинным случаем: а остаток от м неотрицателен при а в отрезке [0, конечное] и конечном ненулевом литерале м. Заводить его всё равно не за чем: тот же обход по корпусу показывает 0 новых закрытых целей, а «В кольцо» из hashmap.flang остаётся незакрытой и с ним — конечность там приходит из (значение минус значение) равен 0, то есть формой, которую ядро фактом не читает.

Общее правило, по которому оба приёма отложены, дерево сформулировало раньше: факт, которым никто не пользуется, — доверие, за которое некому отвечать.

3б-трис. Третий источник фактов: объявленный тип аргумента

Здесь стоял разрыв, который читался как мелочь, а стоил целой строки ведомости. Источников известного у правила неотрицательности было два — литерал не меньше нуля и допущение индукции, — и оба приезжают ИЗНУТРИ доказательства. Объявление параметра не приезжало никак: слов тип, types, typeOf в flang/proof/reduce.mjs было ноль, и это проверялось одной командой (grep -ac "тип\|types\|typeOf" flang/proof/reduce.mjs → 0).

Поэтому постусловие «результат не меньше 0» у функции над двумя нат стояло в ведомости строкой «сетка 1 значение (примеры функции)»: посчитанным на одном входе из 2⁵³ × 2⁵³, хотя доказуемым одним сложением.

**Причина была не в том, что неотрицательно ходит по дереву синтаксически** — она так и должна ходить, это структурная свёртка, и другой ей быть нельзя. Причина в том, что факт из объявления НЕ СТРОИЛ НИКТО: ни обязательства, ни принцип индукции, ни ядро.

Теперь строит известноеПоТипу (flang/proof/reduce.mjs): по одному факту «имя не меньше 0» на каждое имя, объявленное как нат. Имена берутся из ИМЕНА_НАТ типизатора, а не переписаны рядом: второй такой список разошёлся бы молча, и 自然数 перестал бы быть фактом для ядра, оставшись им для типизатора.

Это не аксиома. нат — не имя, а отрезок [0, 2⁵³−1] (types.mjs, NAT): подпись принимает первое: нат и есть написанный автором факт «первое не меньше 0», и типизатор проверяет его на каждом вызове. Ядро этот факт не выдумывает и не выводит — оно читает его там, где он написан. Правило «шаг без названного факта отвергается» не нарушено: факт назван подписью функции. Список АКСИОМЫ по-прежнему пуст.

**Фактом становится только нат.** целое — это [−2⁵³+1, 2⁵³−1], число — вообще всё, включая NaN и −∞; ни то, ни другое о знаке не говорит ничего. Обе подмены стоят изъятиями в flang/test/proof-kernel.test.mjs.

Мест, куда факт приезжает, два, и оба — уже стоявшие:

• Посылка индукции. У каждой посылки принципа появились declarations: параметры функции (кроме переменной индукции — в заключении она уже заменена конструктором) и поля-коэффициенты варианта под именами образца. Тип поля — такой же факт, как тип параметра: вариант «Слой» содержит вес: нат говорит «вес не меньше 0» ровно так же, как принимает вес: нат. Отсюда шаг вида («Вес» от н) плюс вес сводится, а до этой работы отвергался.
• Постусловие БЕЗ теоремы. Оно больше не пропускается молча: ядро делает одну подстановку (тело функции на место результат — ту же самую, какой initial.mjs строит заключение посылки) и один вызов свести. Не свелось — вердикта НЕТ: ни отказа, ни диагностики, и утверждение остаётся сеткой примеров, как стояло. Отказать здесь было бы неправдой: постусловие без теоремы — не ошибка.

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

Ведомость назвала это своим словом. Вердикт несёт поле by: "declaration", свод считает proved-declaration рядом с proved-induction. Сказать «терм принят» здесь было бы неправдой: терма нет вовсе, и шагов в нём ноль.

И ещё одно слово, разведённое с этим позже и по улике. Путь «постусловие без теоремы» закрывает не только цели, где факт дал объявленный тип. Утверждение «результат не меньше 0» у функции над строка, чьё тело — восемь ветвей выбора с литералами, сводится ЦЕЛИКОМ БЕЗ ЕДИНОГО ОБЪЯВЛЕНИЯ: работают литерал и выбор. Пока ведомость печатала на такое «доказано по объявленным типам аргументов», она называла источником факт, которым никто не пользовался, — та же неправда в ту же сторону, что «доказано» вместо «сетки», только мельче. Улика появилась на первом же корпусном утверждении: двух из трёх.

Различает их не строка отчёта, а ЯДРО, и различает ИЗЪЯТИЕМ: proofterm.mjs зовёт свести второй раз, без объявлений, и кладёт ответ в поле byType. Свелось и без них — значит объявленный тип не понадобился, и ведомость говорит «доказано сведением цели с телом функции: объявленные типы аргументов не понадобились». Перебора при этом ноль: второй вызов такой же прямой, как первый. Свод печатает два числа порознь — «без теоремы» и «из них факт дал объявленный тип» (proved-declaration и proved-by-type), — потому что вопросы у них разные, а свернув их в одно, свод потерял бы ровно то различие, ради которого заведён.

Ловушка, на которой это ломается, проверена, а не обещана. Правило верно для суммы и для выбора и ЛОЖНО для разности и произведения. Выдумывать проверку не пришлось: в том же файле корпуса строкой ниже стоит «Разность пары» — те же два нат, первое минус второе, и пример 2 минус 3 = −1 написан там автором языка. Негативных проверок пять: минус, умножить и деление при тех же нат; число и целое вместо нат; подделка в индукции (минус при объявленном нат поле).

3б-кватер. Вторая граница того же объявления: потолок 2⁵³−1

нат — не признак знака, а отрезок [0, 2⁵³−1], то есть ДВА факта на каждое имя. Раздел выше отдал ядру первый. Второй тогда отдан не был, и довод был записан здесь же прямым текстом:

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

Довод был верен ровно до того, как у потолка появился отвечающий. Он появился: граница входа сверяет --args с объявленным типом ДО вычисления (checkArguments, ветка work/entry-types-113). Прежде --args '{"н": 1e300}' втекало в программу молча, и это ломало доказательство ТОТАЛЬНОЙ функции: нат несёт её завершение потолком (ниже 2⁵³−1 н минус 1 точно меньше н, поэтому сторож не печатается вовсе), а 1e300 минус 1 равно 1e300, и цепочка вечна. Теперь значение вне нат до тела не доходит — и потолок стал таким же читаемым фактом, как дно. Верить дну и не верить потолку было бы верой наполовину: держатся оба на одной подписи.

Улика ДО, снятая прогоном. Утверждение «результат не больше 9007199254740991» о «Разности пары» (flang/examples/measure/natural.flang) — ПРАВДА, и написана она в корпусе прозой рукой автора языка строкой над функцией: «А вот РАЗНОСТЬ натуральных остаётся в точной сетке всегда — она может стать отрицательной, но точность не теряет». Типы утверждение проходило (диагностик 0), а ядро на нём молчало: вердиктов 0, свести отвечал «у цели этого случая нет вида, к которому у ядра есть правило».

Теперь строит ограниченноеПоТипу (flang/proof/reduce.mjs): по одному факту «имя не больше 2⁵³−1» на каждое имя, объявленное нат. Число берётся из ТОЧНАЯ_СЕТКА.верх (types.mjs) — из того самого ТОЧНЫЙ_ПОТОЛОК, которым построен сам тип NAT, а не переписывается здесь литералом: переписанное число разошлось бы молча, и ядро отмерило бы отрезок не той длины.

Граница из цели сравнивается, а не подразумевается. Факт даёт имя ≤ 2⁵³−1 и ничего сильнее: цели имя не больше 10 он не закрывает, натуральное бывает и одиннадцатью. Имя попадает в известные, только если спрошенная граница не ниже потолка типа, и граница на единицу ниже потолка отвергается — это проверка, а не рассуждение.

ГЛАВНАЯ ЛОВУШКА, ИЗ-ЗА КОТОРОЙ ЭТУ ПОЛОВИНУ И ОТКЛАДЫВАЛИ: суммы в правиле нет. Потолок — факт про АРГУМЕНТ, а не про результат. Правило дна сумму берёт, и это истинно; правило потолка сумму не берёт, и это тоже истинно: сумма двух нат выходит за потолок законно. Написано это не здесь, а в самом корпусе (flang/examples/measure/natural.flang, раздел 5):

Сложение двух натуральных натуральным быть не обязано: 2⁵³−1 плюс 2⁵³−1 выходит за точную сетку double… Анализ это видит и РАСШИРЯЕТ тип до число.

Перенеси кто-нибудь случай сложения из первого правила в третье — ядро начало бы доказывать ЛОЖЬ о «Сумме пары», стоящей в том же файле строкой выше. Поэтому а плюс б при двух нат с целью «не больше 2⁵³−1» обязано быть отвергнуто, и это отдельная проверка, названная в тесте ГЛАВНОЙ ЛОВУШКОЙ. Изъятие проведено: допиши случай сложения — краснеют две проверки поимённо.

Вычитание берётся — и на двух посылках сразу. а минус б ≤ П выводится из а ≤ П и б ≥ 0, причём вторая посылка спрашивается у правила дна тем же списком известного. Доказательство о IEEE-754: при б ≥ 0 точное а − б не больше а, округление к ближайшему монотонно, а представимо — значит fl(а − б) ≤ а ≤ П. NaN появиться негде: конечное П исключает +∞ у а, б ≥ 0 исключает NaN и −∞ у б, а ∞ − ∞ — единственный способ получить NaN вычитанием. Ровно поэтому граница обязана быть конечным литералом: с границей +∞ правило стало бы ложным.

Убери одну посылку — правило ложно, и обе половины изъяты проверками: вычитаемое число (тогда (2⁵³−1) минус (−5) за потолком), уменьшаемое число (выводить нечего вовсе). Отдельно стоит тонкий случай: **оба целое**. У целое ТОТ ЖЕ потолок, что у нат, — и этого мало, потому что правилу нужно ещё дно вычитаемого, а его целое не обещает. Ядро молчит, и утверждение при двух целое действительно ложно.

Умножения и деления здесь нет, и теперь это расходится с правилом дна намеренно: (2⁵³−1) умножить на 2 за потолком, а частное упирается в деление на ноль. Расхождение списков стало двусторонним — правило дна берёт и сумму, и произведение ограниченных, правило потолка не берёт ни того, ни другого, — и свести их в один список значило бы соврать в обе стороны сразу.

Проверок у правила тринадцать, и негативных среди них больше, чем положительных. Враждебная выборка — близнец той, что стоит у правила дна: 17 значений (включая оба нуля, обе бесконечности, NaN, оба края точной сетки) на 4 границах; правило не нарушено ни разу, а «сумма ограниченных ограничена» нарушается — и это тоже утверждается, иначе список случаев выглядел бы закрытым по лени, а не по доказательству.

3б-квинтэ. Четвёртый источник фактов: РЕЗУЛЬТАТ ВСТРОЕННОЙ ФОРМЫ

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

Улика измерена, а не вспомнена. Обход flang/core и flang/examples (136 функций, у которых «результат не меньше 0» истинно на всех примерах автора) разложил причины отказа по числу, и первые две — свёртка и встроенная длина. На всём корпусе (3838 функций) ядро брало цель у 17.

Факт не выдуман — он уже посчитан типизатором. длина объявлена нат (types.mjs: «счёт элементов конечного дерева неотрицателен и целый по построению»), код символа — отрезком [0, 0x10FFFF] («Unicode кончается на 0x10FFFF, и это граница не IEEE-754, а стандарта»). Ядро читает ту же таблицу (ТИП_РЕЗУЛЬТАТА_ФОРМЫ), а не переписывает числа рядом: разойдись два списка — ядро сочло бы неотрицательным то, что типизатор таковым не считает. Довод тот же, по которому имена нат берутся у типизатора, а не в ядре.

Форм в таблице две из девятнадцати, и остальные семнадцать перебраны поимённо. Перебор стоит исполняемым тестом: список форм берётся у рантайма (BUILTIN_NAMES), и появись двадцатая — она приедет в проверку сама.

Потолка у формы ядро НЕ читает, хотя он в той же таблице. длина объявлена нат, то есть с потолком 2⁵³−1, и правило 3 могло бы взять его тем же чтением. Оно не берёт, и это решение: потолок длины держится не языком, а памятью машины (довод типизатора: «списка длиннее 2⁵³−1 в этой вселенной не существует»), а ставить размер оперативной памяти в цепочку доверия нельзя. Дно же держится построением счёта и верно на любой машине.

3б-секстэ. СВЁРТКА: индукция началом и шагом

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

Индукция у свёртки всё-таки есть; брать её надо не с ветвей, а с самой свёртки: у неё есть НАЧАЛО и ШАГ, и это ровно две посылки индукции по списку.

свёртка над С начиная с Н шагом (а, э) → Т   неотрицательна, если
  Н неотрицательно                                  ← база
  Т неотрицательно при допущении «а не меньше 0»    ← шаг

Это вывод, а не постулат. Значение свёртки есть aₙ, где a₀ — значение Н, а a_{к+1} — значение Т в окружении, где а равно a_к, а э равно (к+1)-му элементу (interpret.mjs, stepFold). Список конечен — обход снимается снимком до первого шага, — значит индукция по его длине законна ровно постольку, поскольку законно допущение о хвосте у принципа индукции: довод один и тот же, «часть значения меньше значения». База: a₀ ≥ 0 по первой посылке. Шаг: пусть a_к ≥ 0; тогда в окружении шага истинно «а не меньше 0», прочие известные факты истинны тоже (их свободных имён свёртка не связывает), и по второй посылке Т не меньше нуля. Пустой список — случай к = 0: результат есть само начало, и о нём говорит база. Список АКСИОМЫ не пополнился ни на строку.

Способов получить отсюда ложь три, и у каждого стоит проверка с контрпримером:

Третья строка — та самая половина инварианта «правило не спускается под связыватель», которая раньше держалась запретом. Запрет снят (в свёртка правило теперь заходит), и держится инвариант вычёркиванием, что строже: у него есть контрпример, а у запрета его не было.

Цена обоих правил измерена изъятием, а не обещана. Охват по всему корпусу (3838 функций, цель «результат не меньше 0»):

Числа не складываются (17 + 13 + 10 = 40, а не 43), и это само по себе улика: трём функциям нужны оба правила сразу — у них свёртка складывает длины.

Из библиотеки этим закрылись два утверждения, стоявшие сеткой: «счёт вхождений неотрицателен» (lists.flang) и «счёт по условию неотрицателен» (higher-order.flang). Ведомость по корпусу: доказано ядром было 29, стало 31; сетка была 19, стала 17, всего высказано 49 — то же самое.

3б-септимэ. Четвёртый ход: ЗАМКНУТАЯ ЦЕЛЬ ВЫЧИСЛЯЕТСЯ

Улика, с которой началось, — две функции без параметров, отличающиеся ровно видом замкнутой цели:

тотальная функция «Число»
  возвращает число
  обеспечивает «ровно сто двадцать восемь» результат равен 128
  128
→ доказано сведением цели с телом функции: правило «тождество после переписки
  допущением» … теоремы при нём нет и не нужно

тотальная функция «Перечень»
  возвращает строка
  обеспечивает «открыт оградой» результат начинается с "|"
  "|нат|натуральное|"
→ объявлено, не доказано: ни теоремы, ни примеров

Замкнуты обе. Разница была не в замкнутости, а в том, что вид первой цели попал в список трёх правил, а вид второй — нет. Считать вторую ничто не мешало: у выражения без свободных имён значение ровно одно.

РЕШАЮЩИХ ПРАВИЛ ПО-ПРЕЖНЕМУ ТРИ, и это проверяется списком, а не прозой (flang/test/proof-kernel.test.mjs: «решающих правил по-прежнему ТРИ»). Вычисление — не правило вывода:

Последняя строка — главная. Ядро уже решает вычислением, и решает им единственное правило, которое закрывает случай целиком: по примеру прогоняет пример тем же интерпретатором, которым язык считает всё остальное. Довод там записан с самого начала: «закрытый терм — это значение, и спорить о нём не о чем, надо посчитать». Здесь тот же довод и тот же интерпретатор; ново одно — место, откуда ход позван. **АКСИОМЫ не пополнились ни на строку.**

Три условия, и ни одно не украшение:

• ЗАМКНУТОСТЬ ПРОВЕРЯЕТСЯ, А НЕ ПРЕДПОЛАГАЕТСЯ. Считает её та же свободныеИмена, какой её считает посылка индукции для по примеру: два ответа на вопрос «какие имена здесь свободны» разошлись бы молча. Осталось хоть одно имя — значений столько же, сколько подстановок, и вычисление одного из них было бы ровно тем сортом лжи, который в этом ядре уже находили.
• ПРЕДЕЛ НАЗВАН (ПРЕДЕЛ_ВЫЧИСЛЕНИЯ — витки и глубина) и при исчерпании отказывает словами: «не досчитали» и «неправда» — разные ответы автору. Состоятельности число не касается: остановиться раньше значит доказать МЕНЬШЕ, а не доказать ложное.
• **ПРИНИМАЕТСЯ РОВНО да.** нет — это ЛОЖНОЕ утверждение, и отказ говорит именно это; не признак — цель не утверждение вовсе; отказ вычисления — цель значения не имеет.

**Вычислитель приезжает в свести ДАННЫМИ**, пятым доводом, — тем же приёмом, каким приезжают определения для развёртки. Не дали вычислителя — хода нет, и ответ свести тот же, знак в знак, каким был до этой работы. На этом стоит сверка с близнецом на flang: она зовёт свести двумя доводами, сличает отказ побуквенно и осталась зелёной целиком.

ДОЛГ НАЗВАН ПРЯМО: у четвёртого хода близнеца на flang НЕТ. flang/self/proof-kernel.flang повторяет три правила и четыре переписки, и сверка с ним честна ровно потому, что ход спрашивается только при переданном вычислителе, а сверка его не передаёт. Написать близнеца этому ходу значит написать на flang вызов интерпретатора flang — то есть не переписать правило, а дать близнецу вычислитель; работа это отдельная и к сведению отношения не имеющая. Пока её нет, справедливо ровно следующее: правила ядра сверены с близнецом целиком, вычисление — нет, и ни одно «доказано» на нём не стоит молча: ведомость называет его своим словом («доказано вычислением замкнутой цели»), а не общим.

Цель отдаётся вычислителю КАК ПРИШЛА, а не нормальной формой. Интерпретатор сам разворачивает пусть, разбор и вызов — правилами языка, а не ядра, — и ход не зависит от нормализации вовсе, в том числе от её ограничителя на захват имени.

Что это дало числом (измерено изъятием теоремы у каждого утверждения, а не оценено): на корпусе ветки work/lemmy ядро закрывало САМО 20 утверждений из 110, стало — 70. Пятьдесят утверждений, которым автор написал и теорему, и пример, перестали требовать и того, и другого; шесть оставшихся требуют индукции, и правильно требуют. На корпусе main число не изменилось (20): целей такого вида в нём просто не было.

И тот же ход закрывает базу индукции. Перечисление из трёх вариантов доказывается теперь ОДНИМ примером вместо трёх: посылки с замкнутым заключением ядро закрывает само и говорит, чем. Дописывание примера на каждый вариант и составляло половину объёма файлов в flang/proof/examples/.

3в. Почему правило сведения — не аксиома

Список АКСИОМЫ по-прежнему пуст, и это не формальность.

Аксиома — утверждение, принятое БЕЗ доказательства; ложная аксиома отравляет всё, что из неё выведено. Правило «сумма неотрицательных неотрицательна» — теорема о IEEE-754, и вот её доказательство целиком: посылка а не меньше 0 истинна только для не-NaN значений из [0, +∞] (NaN не сравним ни с чем, и на нём посылка ложна); сумма двух значений из [0, +∞] под округлением к ближайшему снова лежит в [0, +∞], потому что переполнение даёт +∞, а не отрицательное. Знака терять негде.

Ровно поэтому в списке нет «произведение неотрицательных неотрицательно»: 0 умножить на +∞ даёт NaN, и это утверждение ЛОЖНО. Нет вычитания и деления — по той же причине. И нет х плюс 1 больше х — это и есть тот сорт аксиомы, из-за которого список аксиом пуст.

А умножение при этом в правиле есть, и разница между ним и ложным утверждением выше — ровно одна посылка. Ложным «произведение неотрицательных неотрицательно» делает единственный вход — бесконечность, — и посылка не меньше 0 её не исключает (+∞ не меньше 0 истинно). Исключает её ВТОРАЯ граница той же подписи: нат есть отрезок [0, 2⁵³−1], и потолок ядро читает наравне с дном. Отсюда теорема, которую ядро и применяет:

если а и б каждый не меньше 0 и не больше конечного, то а умножить на б не меньше 0.

Доказательство целиком: посылки оставляют от каждого сомножителя КОНЕЧНОЕ неотрицательное; NaN получить негде (0 × ∞ исключено конечностью, NaN в аргументе — посылкой не меньше 0); точное произведение неотрицательно, а округление к ближайшему монотонно и ноль оставляет нулём, поэтому fl(а·б) лежит в [0, +∞] — переполнение даёт +∞, а не отрицательное.

Посылка требуется от каждого сомножителя и проверяется отдельной свёрткой вОтрезке, список случаев которой короче списка неотрицательности: ни сложения, ни умножения в нём нет, потому что обе операции выводят из отрезка переполнением, а +∞ — ровно то значение, ради исключения которого посылка и заведена. Поэтому н умножить на м при двух нат доказуемо, а (н плюс м) умножить на к — нет. Изъятие проведено трижды: снят случай mul, ослаблена посылка до одной лишь неотрицательности, снята конечность границы — каждый раз краснеют названные проверки.

Третий источник факта — объявленный тип — тоже не аксиома. Имя, объявленное нат или вес, неотрицательно, и вывод состоит из двух проверяемых шагов: (1) оба типа объявлены отрезками с дном 0, и записано это в одном месте (types.mjs, откуда имена импортированы в reduce.mjs, а не переписаны рядом); (2) значение на такой позиции ПРОВЕРЕНО типизатором при каждом вызове — годится пропускает туда только то, чей отрезок вложен в объявленный, а NaN не вложен ни в какой отрезок. Опора названа вслух, как она названа у точного шага в totality.mjs: снимите проверку типов — и это доказательство станет неверным. Это объявленная зависимость одного анализа от другого, а не скрытое допущение.

В списке нет целое: у него дно −(2^53−1), и «не меньше 0» про него ложно. Нет число: у него дна нет вовсе. Список закрыт двумя именами ровно потому, что дно есть ровно у двух типов языка.

Сколько это даёт на настоящем корпусе — считается одной командой, node flang/scripts/weight-gain.mjs: из 139 функций корпуса, которые берут число и возвращают число, ядро выводит «результат не меньше 0» у 4 при нынешних объявлениях (три из них — программа paths/shortest-path.flang, уже написанная на весе; до заведения типа доказуемая была ровно одна) и у 25, если числовые параметры объявить вес. Прирост 21, потерь 0.

Двадцать из двадцати одной — рукописные минимумы и максимумы («Минимум двух», «Максимум двух», «Ограничить» из stdlib/numbers.flang, «Меньшее из» и «Большее из» из self/types.flang, «Минимум трёх» из rosetta/levenshtein-distance.flang и так далее). Это не совпадение: минимум и максимум и есть те две операции, которые образуют на [0, +∞] настоящий коммутативный моноид, — корпус писал их руками задолго до того, как у языка появился тип, на котором о них есть что доказать.

Разница между аксиомой и правилом проверяется, а не обещается: flang/test/proof-kernel.test.mjs перебирает правило по враждебной выборке (оба нуля, NaN, обе бесконечности, MAX_VALUE, MIN_VALUE, EPSILON) и отдельно показывает, что изъятое из списка действительно ложно.

Механизм подсмотрен у datatype-пакета Isabelle (BSD): там принцип индукции тоже порождается из универсального свойства, а не постулируется. Подсмотрен механизм, не код. Ядро Isabelle целиком не переносится, и причина содержательная помимо объёма: Pure — логический каркас, HOL определён поверх него объектной логикой, а наши программы — не термы HOL. Перенеся Pure, мы получили бы проверяльщик термов HOL и задачу погружения семантики flang в HOL — ту же самую, что «выгрузка во внешний прувер». Мы идём другим путём: своё ядро над нашей категорной основой. (Отдельно юридическое: Coq под LGPL-2.1, производная работа от него столкнулась бы с лицензионным контуром проекта — язык под BSD-2. Isabelle под BSD, Lean 4 под Apache-2.0.)

Четыре правила, и каждое решает вопрос без поиска:

• по примеру — утверждение ЗАКРЫТО и вычисляется интерпретатором в да. Закрытый терм это значение, спорить не о чем, надо посчитать. Считает тот же интерпретатор, которым язык считает всё остальное: второго вычислителя нет. «Закрыто» проверяется в обоих местах, где правило работает: внутри индукции — у случая не связано ни одного имени, вне индукции — у функции нет ни одного параметра. Второе условие появилось позже первого и по улике (см. ниже).
• по предположению — утверждение это цель, в которой переменная индукции заменена частью значения, связанной образцом. Ядро его СТРОИТ, а не сличает — единственный способ не дать назвать предположением что угодно.
• по свойству — ссылка на другое постусловие. Ссылка на доказываемое сейчас постусловие отвергается: это круг, и по предположению существует именно затем, чтобы круга не было.
• по закону — факт от закона моноида, монады или изоморфизма. Такой терм принимается, но ослабляет вердикт до сетки: законы посчитаны на конечной сетке автора, а доказательство не может быть сильнее того, на что опирается. Ровно так теряется вся разница между доказанным и посчитанным, если промолчать об этом один раз.

Свод вердиктов — одно правило на всё ядро: слабейшее побеждает, обратного хода нет.

3г. Второй принцип: индукция по ОТРЕЗКУ нат

До этой работы принцип порождался ровно с одного места — с объявления суммы. У нат объявления нет: это встроенное имя, конструкторов у него ноль, функтор читать не с чего. Отсюда следовал соблазн, и назвать его надо прямо: завести аксиому индукции по числу. Она не заведена, и список АКСИОМЫ остался пуст.

Откуда взят принцип. нат — не «неотрицательное число», а ОТРЕЗОК целых [0, 2⁵³−1] (flang/src/types.mjs, NAT). Отрезок КОНЕЧЕН, а у конечного упорядоченного множества всякая строго убывающая цепочка конечна — не по соглашению, а потому что иначе в нём было бы бесконечно много различных значений. Принцип «доказали дно, доказали переход с н минус 1 на н — доказали обо всём отрезке» есть теорема о конечном отрезке, и обе посылки её ядро проверяет, а не принимает на слово.

Где здесь ровно та ловушка, из-за которой аксиом ноль. «х минус 1 меньше х» в IEEE-754 ЛОЖНО при большом |х|: при х = 2⁵³+4 округление к ближайшему возвращает то же самое х. Индукция по числу без верхней границы — эта самая ошибка. Держат её ОБЕ границы объявленного типа, и каждая закрывает свою половину:

Поэтому индукция по число и по целое отвергается, и отказ называет причину числом: у число в носителе живёт +∞, у которого х минус 1 равно самому х (спуска нет вовсе), у целое нет дна. Проверено не рассуждением: 2**53+4-1 === 2**53+4 и Infinity-1 === Infinity стоят равенствами в flang/test/proof-kernel.test.mjs.

Что читается, и ни одного поиска. Пять мест, все написаны автором:

1. тип переменной индукции — в подписи функции;
2. мера — словом убывает. По сумме его писать не надо (убывание следует из построения значения), по числу не следует ничего, и что убывает, обязан назвать автор. Слово в языке уже стояло — девятого слова поверхности принцип по отрезку не потребовал ни одного;
3. условие дна — первым если по переменной индукции. Форм пять, список закрыт: п не больше К, п меньше К, п равно 0, п больше К, п не меньше К. У двух форм (п меньше К и п не меньше К) К обязан быть целым: верх дна у них считается как К минус 1, и при дробном К этот верх ВРЁТ. Это не осторожность, а починка найденной дыры: если н меньше 2.5 при н: нат отправляет в базу и н = 2, а посылка базы получала факт «н не больше 1.5» — и ядро печатало «доказано индукцией» об утверждении, которое рантайм тут же отвергал FLANG_PROPERTY на н = 2. Теперь такая запись отвергается кодом FLANG_PROOF_INDUCTION_BRANCH, и подделка стоит проверкой;
4. какая ветвь база — ФОРМОЙ условия, а не догадкой о содержимом ветви;
5. на чём стоит рекурсивный вызов — аргументом вызова.

**Факты посылок читаются с того же если, и их ДВА, а не один.** База получает п не больше верх, шаг — п больше верх: в ветвь спуска вычисление попадает ровно тогда, когда условие дна ложно. Это не вывод и не догадка, а вторая половина той же прочитанной формы, и для всех пяти записей она пишется одинаково — вот построчная сверка:

Факт шага — единственный источник строгой положительности во всём ядре (раздел 3б), и без него не замыкается ни одно рекурсивное умножение.

Что ядро проверяет, а не принимает на слово: СПУСК. Аргумент рекурсивного вызова обязан быть н минус 1 и ничем иным. н плюс 1, н минус 0, вызов на самом н, н минус 2 — отвергаются кодом FLANG_PROOF_INDUCTION_DESCENT. Код свой, а не общий с шагом, и это не мелочь: «шаг не сведён к допущению» и «спуск, на котором стоит допущение, никуда не спускается» — разные находки и разные починки; вторая означает, что доказательства не было вовсе.

**Образцы у отрезка — те же, что у разбор, и своих не заведено.** Дно — это случай 0 (литерал, попадающий в дно), спуск — случай любое. Имени у любое быть не должно: связывать нечего, значение одно и уже названо переменной индукции.

Живой пример: flang/proof/examples/segment.flang — две функции над нат, обе доказаны. У первой базу закрывает само ядро и случая при ней нет; у второй дно написано случай 0 и закрыто примером, и ядро сверяет, что значение примера в дно попадает.

Сколько корпуса этим взялось — измерено, а не предположено, и мерка та же. Здесь стояло: «у 31 функции корпуса есть параметр нат; у 17 принцип по отрезку ЧИТАЕТСЯ целиком; обе посылки не сводятся сегодня ни у одной», и дальше — что шесть функций возьмутся, «как только правило умножения появится». Правило появилось, и половина предсказания оказалась верной, а половина нет. Обе половины измерены одним обходом (flang/proof/initial.mjs и свести на каждой посылке), и числа такие:

Девять — это две прежние фикстуры, новый corpus-factorial.flang и ШЕСТЬ настоящих функций корпуса: «Факториал» на всех четырёх поверхностях, «Факториал» из flang/examples/measure/natural.flang и «Факториал» из flang/stdlib/numbers.flang.

Но написать утверждение и теорему можно только у ТРЁХ из этих шести, и препятствия к ядру доказательства отношения не имеют ни одно:

• factorial.eo.flang и factorial.zh.flang — восьми слов доказательства у эсперантской и китайской поверхностей НЕТ ВОВСЕ (flang/src/lexer.mjs, «ВОСЕМЬ СЛОВ ДОКАЗАТЕЛЬСТВА без эсперанто и без китайского»). Утверждение о тех файлах не высказать — не «не доказать», а именно не высказать;
• stdlib/numbers.flang «Факториал» — параметр назван число, а это КЛЮЧЕВОЕ СЛОВО (тип). Постусловие пишется (для всех число обеспечивает …), а дано число: нат и индукция по число разбору не поддаются вовсе.

Всё это стоит исполняемыми проверками в flang/test/corpus-claims.test.mjs, а не словами: заведись эсперантское слово или переименуйся параметр — тесты покраснеют и потребуют переписать этот абзац.

А «Степень» из предсказания надо вычеркнуть, и не потому, что ядро не тянет. Утверждение «результат не меньше 0» о ней ЛОЖНО: основание объявлено число, и «Степень» от (0 минус 2) и 1 равно −2. Доказывать там нечего.

Остальное упирается по-прежнему НЕ в индукцию: у «Фибоначчи шагом» и «Ступени шагом» спуск сводится допущением, а дно ЛОЖНО — накопитель объявлен число, и «результат не меньше 0» о них неправда («Фибоначчи шагом» от 0 и (−7) и 9 равно −7).

3д. Три ФОРМЫ ТЕЛА, за которые принцип цепляется (16 августа 2026)

Улика ДО, числом. Замер цены доказательства (docs/zamer-tseny-2.md) назвал узкое место со знаменателем: заключение посылки индукции ядро строило ТОЛЬКО с ветвей разбор по переменной индукции. Таких тел в flang/stdlib 58 из 208. Остальные 150 написаны свёрткой (45), условием (37), арифметикой (21), вызовом (18), встроенной формой (9), пусть (8), отображением и отбором (8), построением (3), применением (1). То есть 72 % библиотеки написано формами, к которым принцип не цеплялся ничем, и отказ на всех был один и тот же: FLANG_PROOF_INDUCTION_BRANCH. На двадцати функциях замера — 7 отказов из 18.

Ходов прибавилось три. Решающих правил по-прежнему ТРИ, аксиом ноль.

Ход пятый: РАЗБОР ЦЕЛИ ПО УСЛОВИЮ

Цель, у которой на верхнем уровне стоит если, делится надвое подстановкой ЗНАЧЕНИЯ условия, и обе половины сводятся теми же тремя правилами.

Законно это потому, что условие У — выражение типа признак (проверил типизатор), а у признака значений ровно два. Значит цель совпадает либо с собой, где У заменено на да, либо с собой, где У заменено на нет. Доказав обе, доказали цель.

Это НЕ то, что уже измерено нулём. docs/zettel/usloviya-esli-dali-nol.md записывает: чтение условий если КАК ФАКТОВ закрывает ноль целей, и ветвь иначе читать нельзя вовсе — на не число ложны обе стороны сравнения, и из «не (х меньше у)» не следует «х не меньше у». Здесь НИ ОДИН факт из условия не выводится: подставляется значение. Ловушка не число про перевод отрицания сравнения в другое сравнение, а здесь отрицания нет.

Границы, и каждая в коде:

• не под связывателем. Условие берётся только с того если, до которого обход дошёл, ни разу не войдя внутрь разбор, свёртка, отобразить/отфильтровать, пусть. Под связывателем у выражения нет одного значения. Тем же обходом ограничена и ЗАМЕНА.
• предел. ПРЕДЕЛ_ВЕТВЛЕНИЯ = 4. Каждое деление удваивает число целей; самое глубокое вложение условий в корпусе — три. Достижение предела говорит о себе словами.
• половина закрыта двумя способами и только ими: сведена теми же правилами или стала литералом да. Ставшая литералом нет — ЛОЖНА, и отказ говорит это.

Ход шестой: ИНДУКЦИЯ ПО СВЁРТКЕ

Тело свёртка <переменная индукции> начиная с И как а и э → Т даёт две посылки: начало (заключение P(И)) и виток (заключение P(Т) при допущении P(а)).

Сказать надо прямо: это НЕ индукция по списку. Свёртка в flang ЛЕВАЯ (interpret.mjs, stepFold), и её второе определяющее уравнение

свёртка (г : х) начиная с И как а и э → Т = свёртка х начиная с Т[а:=И, э:=г] …

меняет НАЧАЛО, а не только список. Допущение по списку говорило бы о свёртке хвоста при том же начале, заключение — о свёртке хвоста при другом начале, и свести одно к другому нечем. Это свойство левой свёртки, а не пробел ядра: доказательство по списку потребовало бы обобщения утверждения по накопителю, то есть ПОИСКА ИНВАРИАНТА, которого у ядра нет и не будет.

Читается вместо этого принцип по числу ВИТКОВ: витков ровно столько, сколько ячеек в списке (длина снимается один раз, до первого витка), утверждение, истинное о начале и переживающее виток, истинно о результате. Тот же ход уже жил ВНУТРИ правила неотрицательности (неотрицательнаяСвёртка); эта работа вынула его в построение посылки, чтобы им пользовались все три правила.

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

Три отказа, и каждый закрывает способ получить ложь: имена накопителя и элемента обязаны быть разными; ни одно из них не имеет права быть свободным в самой цели; объявленные типы этих имён в посылки не едут.

Ход седьмой: СЛИЧЕНИЕ ПО ВЫЗОВУ

по свойству «имя» существовало на поверхности с самого начала и отказывало всегда: «свести „результат“ шага с результатом другой функции ядру пока нечем… дождитесь сличения по вызову». Дождались.

Факт — не вера: вычислитель проверяет постусловие ПОСЛЕ КАЖДОГО возврата (interpret.mjs, stepPost), и нарушенное постусловие прекращает вычисление отказом FLANG_PROPERTY. Значит у вызова, у которого есть значение, постусловие вызываемого на этом значении истинно. Ядро читает написанное слово — ровно так же, как читает тотальная, разворачивая вызов. Оговорка та же, что у правила неотрицательности: у вызова без значения утверждение не истинно и не ложно, оно не высказано.

ОТ ЧЕГО ЭТОТ ХОД ЗАВИСИТ, СКАЗАНО ЗАРАНЕЕ. Он опирается на то, что постусловие ЛИБО доказано ядром, ЛИБО проверяется на каждом возврате. Первый пункт списка недостающего (docs/lemmy-otchet.md) предлагает «не проверять доказанное постусловие в рантайме» — и это ход СОВМЕСТИМЫЙ: снимается проверка ровно с того, что доказано, а недоказанное остаётся под проверкой. А вот снять проверку с НЕДОКАЗАННОГО постусловия нельзя, не сломав это правило, и здесь это записано затем, чтобы поломка не прошла молча.

Подстановка ЧИТАЕТСЯ: в заключении ищутся узлы вызов «Г» от …, и на каждом постусловие «Г» инстанцируется двумя подстановками — параметры на аргументы ЭТОГО вызова, результат на сам вызов. Кандидатов столько, сколько вызовов. Нет ни одного вызова «Г» — отказ говорит именно это. Круг (ссылка на доказываемое сейчас постусловие) остаётся запрещён. Выписанное автором утверждение шага обязано быть заключением этого места, иначе посылка считалась бы доказанной по тому, что к ней не относится.

Долг назван прямо: у ходов пятого и шестого близнеца на flang НЕТ

Ход разбора по условию включается ШЕСТЫМ доводом свести (витков), и ноль по умолчанию значит «хода нет» — тем же приёмом и по той же причине, что у четвёртого хода. Поэтому побайтовая сверка с близнецом осталась зелёной целиком: она зовёт свести двумя доводами. Справедливо ровно следующее: три правила сверены с близнецом, вычисление, разбор по условию и индукция по свёртке — нет, и ни одно «доказано» на них не стоит молча: ведомость называет каждый ход своим словом.

Что это дало числом

Подделки и изъятия на каждый ход — flang/test/proof-forms.test.mjs, 15 проверок. Пример корпуса — flang/proof/examples/body-forms.flang.

Граница честности: что ядро доказывает целиком

Рекурсивный случай доказывается. Это и есть та работа, ради которой писался слой начальной алгебры, и потолок языка ею снят: утверждение о функции над бесконечным типом теперь может стоять в ведомости словом «доказано», а не «сеткой N значений автора». Живой пример: flang/proof/examples/stack.flang — два утверждения о «Стопке», у которой значений бесконечно много, доказанные двумя посылками каждое.

Что ядро доказывает целиком:

1. Утверждения о конечной сумме, закрытые в каждом случае — перечисления, у которых все конструкторы без полей. База закрывается вычислением примера. Пример: flang/proof/examples/traffic-light.flang.
2. Утверждения о рекурсивной сумме, у которых заключение шага сводится к допущению одним из двух правил (раздел 3б). Примеры: flang/proof/examples/stack.flang и четыре corpus-*.flang — настоящие функции корпуса «Высота», «Размер дерева», «Глубина» и «Глубина дерева», перенесённые дословно.
3. Утверждения, у которых заключение шага говорит о результате ДРУГОЙ функции — если её определение разворачивается (раздел 3б-бис). Примеры: «высота копии равна высоте оригинала» в stack.flang (развёртка по конструктору) и corpus-tree-depth.flang — «Глубина дерева» из flang/stdlib/tree.flang, чей шаг упирался в «Глубже» (плоское определение).
4. Утверждения о функции, рекурсивной ПО ЧИСЛУ — индукцией по отрезку нат (раздел 3г). Примеры: flang/proof/examples/segment.flang и corpus-factorial.flang — настоящий «Факториал» из flang/examples/rosetta/factorial.flang, перенесённый дословно вместе со всеми четырьмя примерами. Спуск при этом проверяется, а не принимается: подделка, у которой шаг не убывает, — отвергается.

4-бис. Утверждения, у которых шаг стоит на УМНОЖЕНИИ рекурсивного вызова. Это то место, где встречаются оба принципа этого раздела, и закрылось оно двумя чтениями сразу: посылка шага читает свой если (п больше верх), а у умножения появилась вторая посылка (один сомножитель в (0, конечное]). Ни одного нового слова поверхности и ни одной аксиомы это не потребовало.

1. Посылку, которая сводится БЕЗ ЕДИНОГО ДОПУЩЕНИЯ ИНДУКЦИИ — и закрывает её само ядро, без случая при ней. Так закрыт долг «базу нечем закрыть, кроме примера»: «Глубина» из flang/examples/leetcode/104-… доказывается теперь БЕЗ единой дописанной строки, а её копия в corpus-depth.flang перестала нести пример, которого в корпусе нет.
2. Утверждение, цель которого ЗАМКНУТА, — каким бы ни был её вид (раздел 3б-квинт). Свободных имён нет — значение одно, и вычисление отвечает про него целиком. Сюда попадает всё, о чём у ядра правила нет и не предвидится: начинается с, входит в, длина, свёртка по таблице. На корпусе work/lemmy это 50 утверждений, у которых теорема и пример перестали быть нужны.

1. Утверждения о функциях над ВСТРОЕННЫМ списком — тем же принципом и теми же двумя правилами (раздел 3а-бис). Три доказаны на настоящих функциях библиотеки: «длина неотрицательна» и «индекс неотрицателен» о flang/stdlib/lists.flang, «позиция неотрицательна» о flang/stdlib/higher-order.flang. Два последних — на функциях ДВУХ параметров, а третье — на функции, у которой первый параметр сам функция: она проезжает посылку коэффициентом и индукции не мешает.

Что ядро НЕ доказывает и отвергает вслух:

• Случай, в заключении которого осталось свободное имя, поданный примером. Пример — одно значение, а у незакрытого заключения их столько же, сколько подстановок. Проверяется заключение, а не образец, и это исправление, а не формулировка: проверка образца ошибалась в обе стороны сразу. Слишком слабо — у функции двух параметров образец случай пусто не связывает ничего, а в заключении оставался второй параметр (случай пусто то н при цели «результат не меньше 0» давало ЛОЖНОЕ н не меньше 0 и закрывалось примером с н = 5). Слишком сильно — образец со связанными именами при теле-литерале даёт закрытое заключение, и отказывать ему значило требовать доказательства у вычисленного. Обе стороны стоят негативными тестами в flang/test/proof-kernel.test.mjs, и ложность первой измерена рантаймом на н = −1, а не рассуждением.
• Утверждение о функции С ПАРАМЕТРАМИ, поданное примером ВНЕ индукции. То же правило и та же причина, но проверки здесь не было: она стояла только в ветви случая, а доказательство без индукция по случая не имеет вовсе. Найдено программой, а не чтением: постусловие «Длина» от результат равен 3 у «Соединить списки» — утверждение обо ВСЕХ парах списков, ложное почти на всех, — получало вердикт «доказано ядром: терм принят, 1 шаг», потому что пример «Два непустых» и правда даёт три. Примером закрывается только утверждение с ОДНИМ значением, то есть функция без параметров; изъятие и обратная половина (функция без параметров принимается по-прежнему) стоят в flang/test/proof-kernel.test.mjs.
• Цель, в которую подстановка ЗАХВАТИЛА БЫ имя. Подстановка результат := <тело> вычёркивала связанное имя КЛЮЧА и не смотрела на имена ЗНАЧЕНИЯ, а докстринг подставить утверждал прямым текстом «захвата здесь быть не может». Цель со свёртка … как акк и х → результат получала на место результат тело, свободное в х, и х уезжал под чужой связыватель: снаружи параметр функции, внутри элемент свёртки. Цель (свёртка [1] начиная с 0 как акк и х → результат) равно (свёртка [1] начиная с 0 как акк и х → х) означает «результат равен 1»; после захвата обе стороны становятся одним термом, и правило тождества сходится знак в знак. Ловилось на обоих путях сразу — и без теоремы («доказано сведением цели с телом функции»), и С НЕЙ («доказано ИНДУКЦИЕЙ по «Дерево» … обо ВСЕХ входах типа «Дерево»»), причём во втором случае захват ещё и ПРЯТАЛ свободное имя от проверки посылка.free: связанное свободным не считается, значит базу пускало правило по примеру, а пример автора честно проходил — он написан на значении, где утверждение случайно верно. Шаг при этом сводился по-настоящему: ложь пролезла не через дырявое правило сведения, а через дырявую подстановку ПЕРЕД ним. Починка — ОТКАЗ, а не переименование, по той же причине, что у развёртки: выдуманное имя не сличить с допущением. подставить спрашивает захватывает и возвращает null, а ядро читает null как «заключения нет». Отказ называет причину отдельно от «нет ветви разбора»: обе кончались одним conclusion === null, и по первому сообщению автор пошёл бы править тело функции, которое в порядке. Обе улики и обе границы — в flang/test/proof-soundness.test.mjs. Близнец починен вместе с эталоном, и сверка перестала быть слепой к этому. Молчала она не по доброте: у неё было 90 входов подстановки и ни одного с захватом — затенение КЛЮЧА стерегли, имена ЗНАЧЕНИЯ нет. Входов стало 176, по одному на каждый из четырёх связывателей плюс обратная половина (связыватель назвал ДРУГОЕ имя — подстановка обязана пройти). Изъятие показывает цену: снимите захват у близнеца — сверка краснеет 12 расхождениями из 176, а до новых входов показывала 0 из 90.
• Спуск по числу, который не убывает — код FLANG_PROOF_INDUCTION_DESCENT (раздел 3г), и это главная негативная проверка второго принципа.
• Шаг, не сводящийся тремя правилами. Отказ называет правило, которое не прошло, и код FLANG_PROOF_INDUCTION_STEP.
• Посылку, у которой связанное имя непрозрачного поля ПОПАЛО В ЗАКЛЮЧЕНИЕ — например «Есть» содержит значение: «А», когда тело ветви это значение возвращает. Допущения там нет (поле не типа самой суммы), а примером случай не закрыть (имя свободно). Это ближайшая оставшаяся граница, и закроет её не индукция, а упрощатель (раздел «Что дальше»).
• Индукцию по строке — хотя её разбор исчерпывается теми же двумя образцами, что у списка. Функтор у строки другой, и алгебра ей не дана нарочно (раздел 3а-бис).
• **Ссылку по свойству на постусловие другой функции** — по-прежнему, и по той же причине: сличение по вызову не сделано. Развёртка этого НЕ закрыла и не могла: она читает ТЕЛО чужой функции, а по свойству ссылается на её ОБЕЩАНИЕ. Вещи разные: тело есть у всякой функции, обещание — только у той, у которой автор его написал, и опереться на обещание можно там, где тело разворачивать нельзя (рекурсия, нат, чужой модуль).
• Развёртку вызова на неизвестном значении — «Копия» от х при связанном х, «Фибоначчи шагом» с рекурсией по числу. Ограничители названы в разделе 3б-бис, и оба случая стоят проверками.

Подделка отвергается, и это проверено. Неверное утверждение, поданное с тем же самым доказательством индукцией, которое проходит на верном, ядро отвергает — причём база подделки честно проходит, и ложь видна только в шаге. Это главная негативная проверка файла flang/test/proof-kernel.test.mjs; без неё слой был бы машинкой, штампующей слово «доказано».

Аксиом у ядра по-прежнему ноль (АКСИОМЫ пуст). Почему правила сведения ими не являются — раздел 3в.

Ядро — тотальная программа flang, и это показано прогоном

Свойство, ради которого ядро своё, а не чужое: проверяльщик термов — структурная свёртка по КОНЕЧНОМУ дереву, то есть идеальная тотальная программа flang.

Близнец ядра на самом языке лежит в flang/proof/kernel.flang. Что о нём говорит flang check --proof:

  «Слабее»                            доказано композицией: рекурсии нет
  «Вердикт шага»                      доказано композицией: рекурсии нет
  «Вердикт цепочки»                   доказано структурой: аргумент 1 («звенья»)
                                      на каждом витке становится частью себя
  «Вердикт случаев»                   доказано структурой: аргумент 1 («случаи»)
                                      на каждом витке становится частью себя
  «Вердикт половины»                  доказано композицией: рекурсии нет
  «Вердикт непокрытого»               доказано композицией: рекурсии нет
  «Вердикт индукции»                  доказано композицией: рекурсии нет
  «Вердикт доказательства»            доказано композицией: рекурсии нет
  «Вердикт доказательства индукцией»  доказано композицией: рекурсии нет
итог: функций 9: тотальных 9, обычных 0; сторожей в рантайме: 0 мест

Свёртка принципа индукции живёт здесь же, на самом языке, и это условие работы, а не украшение: припиши кто-нибудь свёртку принципа только в эталон — сверка молча стала бы проверять половину ядра. Индукция при этом не потребовала ни одного сторожа: четыре новые функции не рекурсивны вовсе, а две прежние как убывали структурно, так и убывают. Если бы принцип потребовал счётчика глубины или предела шагов, это значило бы, что сделано не то.

Носитель обещания у рекурсивных функций — СТРУКТУРА, и это сильнее, чем просто «тотальна»: с мерой или постоянным шагом тотальность тоже бывает, но со сторожем, а сторож — место, где программа честно откажет вместо ответа. У свёртки по конечному дереву такого места нет. Ядро печатается во все восемь целей.

Вердикты близнеца сверены с вердиктами эталона на 3282 порождённых термах цепочек и 133 956 термах принципа индукции, расхождений 0 (flang/test/proof-kernel-twin.test.mjs) — тем же приёмом, которым в этом дереве сверяются девять исполнителей.

У сверки принципа прочтений три, а не два: близнец на flang, эталон, записанный в тесте заново, и свернутьПринцип из ядра. Третье не лишнее — ядро сворачивает принцип по ВЕРДИКТАМ посылок, а близнец по пометкам шагов, и не сойдись они, ведомость печатала бы «доказано индукцией» там, где близнец сказал бы «отвергнуто».

Что эта сверка не доказывает. Она не доказывает состоятельности ядра. Совпадение двух реализаций ловит ошибку в одной из них; общая ошибка проекта останется общей. Поэтому о результате говорится ровно с той силой, какая у него есть: «перекрёстно сверено на N термах», а не «ядро состоятельно». Это та же дисциплина, по которой в ведомости запрещено слово «проверено» вместо «доказано».

Близнец есть и у РЕШАЮЩЕЙ половины, а не только у свёртки пометок

flang/proof/kernel.flang выше сворачивает уже расставленные ПОМЕТКИ шагов в вердикт. Кто расставил пометки — то есть кто решил, выведен шаг или нет, — до этой работы оставалось на JavaScript целиком: 1306 строк, initial.mjs (399) и reduce.mjs (907). Это и есть то место, где решается, что считается доказательством, и близнеца у него не было.

Теперь есть, обеими половинами:

Близнец знает ВСЕ ТРИ решающих правила и ВСЕ ЧЕТЫРЕ переписки нормализации, и это стоило отдельной работы: на первом переносе он унёс два правила и три переписки, а зазор был измерен прогоном — правило потолка расходилось на 450 утверждениях из 2268, развёртка на 27 из 144. Оба числа теперь ноль.

Критерий у первой сверки не «принято/отвергнуто», а вердикт, имя правила, текст причины и отчёт о развёрнутом — знак в знак. Довод тот же, по которому печать сверяется побайтово: два ядра могут принять одно и то же РАЗНЫМИ правилами и разойтись на первом же утверждении, которого в корпусе не было. Имя правила и текст причины уезжают в отказ к автору доказательства; разойдись они, автор чинил бы не то, что сломано.

Подделка отвергается близнецом так же, как эталоном — тем же правилом и тем же текстом. Проверено обеими подделками: тело шага, вычитающее вместо сложения (правило 1), и функция, объявленная тождественной и таковой не являющаяся (правило 2).

И каждое правило доказано изъятием, а не обещанием. Шесть подмен в копии близнеца: сложение в правиле потолка (оно доказало бы ЛОЖЬ о «Сумме пары» из корпуса), снятое сравнение границы с потолком типа («нат» стал бы десяткой), снятое «только тотальное», снятая проверка захвата имени, замолчанный рассказ о достигнутом пределе и потерянная протяжка состояния нормализации. Сам предел изъять нельзя: без него проверка не покраснела бы, а ЗАВИСЛА.

Круг замкнут на том куске пути, который перенесён. Принцип строит близнец, сводит его близнец, и вердикт каждой из 16 посылок корпуса совпадает с вердиктом двух эталонов на том же входе. Проверка отдельная от сверки вердиктов, и это не дублирование: сверке вердиктов термы даёт ЭТАЛОН, поэтому она молчала о том, что близнец начальной алгебры не строит поля declarations вовсе. Нашла это побайтовая сверка принципа, а закрывает пятно третья проверка.

СВЯЗКА ПЕРЕНЕСЕНА, И ЭТО НАЗВАНО ЧИСЛОМ. Здесь стояло «между поверхностью и двумя перенесёнными половинами стоят ещё 1281 строка JavaScript». Стоят ноль:

Критерий у обеих сверок побайтовый, и это не перестраховка. Обязательство — ДАННЫЕ, которые читает ядро (goal, bind, vars, hypotheses, forall): ошибись близнец в одном поле, и ядро честно свело бы ДРУГУЮ цель и честно сказало бы «доказано» о том, чего автор не обещал. У вердикта же сверяются и код отказа, и его ТЕКСТ: код уезжает в инструмент, текст к автору доказательства, и разойдись любой из двух — автор чинил бы не то, что сломано.

Отказы сверены не на дереве, а на программах, написанных под каждый отказ. В дереве нет ни одной теоремы, доказывающей не то, и ни одного невыводимого шага — и не должно быть. Поэтому корпус сверки дописан руками: семь кодов связки (NO_GOAL, AMBIGUOUS, DUPLICATE, CLAIM_MISMATCH, UNKNOWN_VAR, VAR_TYPE, UNFINISHED) и пять кодов ядра (STEP, INDUCTION_CASES, INDUCTION_STEP, INDUCTION_TYPE, INDUCTION_BRANCH), и отдельная проверка требует, чтобы все двенадцать на корпусе СРАБОТАЛИ: «обе стороны молчат» — тоже совпадение, и принимать его за сверку нельзя.

Одно место, где дословный перенос НЕВОЗМОЖЕН, и оно названо причиной. Исход прогона примера (по примеру «имя») приезжает в близнеца ДАННЫМИ, а не считается им. Причин две, и обе — свойства языка: исключений в flang нет вовсе (эталон ловит ошибка.message интерпретатора JavaScript), а «Прогон» вычислителя на flang объявлен ОБЫЧНЫМ намеренно — вычисление чужой программы завершаться не обязано, а нетотальность заразна по вызову, и слой, печатающий «доказано», звать его не вправе. Приём тот же, каким в self/proof-kernel.flang приезжают определения функций. Все остальные решения — сличение случаев с конструкторами, раздача посылок правилам, вызов сведения, свёртка пометок в вердикт — принимает близнец.

Что это меняет и чего не меняет. Меняет: слова «доказуемость при наличии Node» больше не обязательны — вся цепочка от постусловия до вердикта существует на самом flang. Не меняет: ни одно ПРЕЖНЕЕ утверждение корпуса не сменило вердикта и не сменило слов — индукцией по-прежнему 8, по объявленному типу 3, сеткой 1, объявлено и не доказано 1, шагов в принятых термах 18, отвергнутых 0. Перенос ничего не доказал заново.

Прибавилось ровно два утверждения (31 → 33 высказано, 29 → 31 доказано), и оба — следствие ПРАВИЛА КОРПУСА, а не переноса правил. Каждый слой близнеца называет версию своего формата нуль-арной функцией с литералом, ядро сводит у такой функции «результат не меньше 0», а flang/test/corpus-claims.test.mjs требует, чтобы такая функция в каталогах побайтовой неподвижной точки несла утверждение там же, где стоит. Два новых слоя дали две новые версии формата — и два утверждения при них.

Эталон ушёл вперёд, пока писался близнец, и зазор ИЗМЕРЕН. Близнец писался под эталон своего основания. Пока он писался, сборщик влил в main работу над САМИМ ядром: эталон ядра там вырос на 443 строки, и прибавка не косметическая — у принципа индукции появился ТРЕТИЙ источник (отрезок объявленного нат), у встроенного списка появилась начальная алгебра, у отказов прибавился код descent, в правила сведения вошло умножение при условии.

Мерено прогоном, а не оценено: на корпусе main (189 программ, 44 строки ведомости) вердикт близнеца расходится с эталоном main на ЧЕТЫРЁХ программах, и ещё на ШЕСТИ решение то же, а текст или поля разошлись. Все десять — про то, чего в основании не было вовсе: индукцию по числу и по встроенному списку. У self/obligations.flang зазора нет вовсе: src/obligations.mjs на main отличается одним словом export.

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

Что ещё держит эталон, названо там же, где считается: flang check --proof (flang/bin/flang.mjs) зовёт JavaScript-половины, а не близнецов; перевод AST в «Значение» и обратно живёт в сверках, а не в дереве; и восемь целей печати близнецов связки пока не печатают.

Два места, где дословный перенос дал бы ПРОТИВОПОЛОЖНЫЙ ответ. Эталон сличает узлы через ===; -0 === 0 истинно, а равен языка работает через Object.is и говорит «нет». NaN === NaN ложно, а Object.is(NaN, NaN) истинно. Ноль цели «Е не меньше 0» сличается именно этим сравнением, поэтому близнец сличает числа двойным «не меньше», а не равен. Оба места стерегутся изъятием.

Найдено сверкой, и это про корпус, а не про близнеца. Порядок двух подстановок в заключении посылки назван значимым здесь и в шапке initial.mjs (тело ветви вправе упоминать переменную индукции), но входа с такой записью в proof/examples/ НЕТ НИ ОДНОГО: изъятие внутренней подстановки проходит незамеченным на всех шести доказательствах корпуса. Пример пришлось написать в тесте.

Сторож на класс: «доказано обо ВСЕХ входах» против прогона

Сверка близнецов состоятельности не доказывает — это сказано абзацем выше и остаётся правдой. Есть и вторая причина завести проверку другого рода: точечный тест ловит ТУ дыру, которую видел его автор. За одни сутки ядро ШЕСТЬ раз напечатало «доказано» о неправде, и каждый раз дыра была новая:

1. дробное дно отрезка (work/kernel-factorial);
2. незамкнутая цель под ПРЯМЫМ по примеру (замер work/zamer-tseny);
3. свободный ВТОРОЙ параметр в базе индукции — та же проверка, другой вход;
4. захват имени под отфильтровать при РАЗВЁРТКЕ определения;
5. захват имени при ПОДСТАНОВКЕ цели, без всякой развёртки;
6. тот же захват через ИНДУКЦИЮ — «доказано индукцией … обо ВСЕХ входах типа «Дерево»» об утверждении, которое рантайм отвергает на первом же значении.

Каждая закрыта своим тестом, и каждый такой тест смотрит ровно туда, куда смотрел его автор.

Общего у всех шести ровно одно, и это не место: проверка состоятельности БЫЛА, а один вход в неё её не звал. Прямой шаг не заходил в ветку случая; проверка случая смотрела на образец, а не на заключение; сторож захвата знал три связывателя из четырёх; подстановка стерегла имя ключа и не смотрела на имена значения. Место у каждой своё, класс один — и сторож написан на класс.

Поэтому у слоя есть проверка не на место, а на СВОЙСТВО (flang/test/proof-soundness.test.mjs):

если ведомость говорит об утверждении «обо ВСЕХ входах», то прогон не находит контрпримера ни на одном значении враждебной сетки.

В этом условии нет ни слова про по примеру, про индукцию, про правила сведения и про чтение объявленного типа: новое правило ядра попадёт под него само, без единой правки в тесте.

Сетка читается с объявлений, а не угадывается. Скаляры — враждебной выборкой (ноль и минус ноль порознь, NaN, обе бесконечности, дробное, пустая строка); объявленные суммы — тем же чтением конструкторов, каким порождается принцип (initial.mjs). У нат сетка лежит ВНУТРИ отрезка [0, 2^53−1]: значение вне него рантайм отвергает FLANG_TYPE («вне нат»), и контрпримером оно не является — утверждение о нём и не высказывалось. Функция-значение приезжает из примеров автора: годятся только теги, которые программа где-то берёт значением.

Контрпример отличается от прочих отказов по СООБЩЕНИЮ, а не по коду. FLANG_PROPERTY носит и чужое постусловие, всплывшее из вложенного вызова; а «предел шагов», «вне нат» и «встроенная форма на пустой строке» говорят, что вычисление не дошло, — это не опровержение.

Проверяются ВСЕ утверждения корпуса, а не только доказанные. Сперва сторож отбирал по вердикту, и довод к отбору был верен про вердикт и неверен про утверждение: «сетка» об ВСЕХ входах ничего не обещает — но само утверждение под ней либо правда, либо нет. Разницу показал корпус. В four-words.flang — файле, который УЧИТ читать слова ведомости, — два утверждения были ложны («результат не меньше 0» о функции над обычным число, контрпример −1), а ведомость печатала «сетка 3 значения: нарушений не найдено» и «объявлено, не доказано». Обе строки правда о себе, а пара читается как заверение. Нашли это независимо ветка work/trebuet чтением и сторож прогоном.

Поэтому вердикт теперь не отбирает, а НАЗЫВАЕТСЯ рядом с находкой: по нему читается, что чинить — «доказано» о лжи есть дыра в ядре, «сетка» о лжи есть неправда в самом утверждении. Порог у обоих один: контрпримеров ноль.

Числа: утверждений корпуса 60, покрыто сеткой 60, значений прогнано 2121, опровергнутых 0. Охват стоит числом и краснеет: проверка вида «для всех верно X» зеленеет и при нуле проверенных, а непокрытый параметр называется поимённо.

Зубы показаны отдельно. На всех ПЯТИ подделках — прямой шаг при цели с параметром, база индукции при свободном втором параметре, захват имени при развёртке под отфильтровать, захват при подстановке цели и он же через индукцию — сетка контрпример НАХОДИТ. Изъятие каждой проверки ядра красит поимённо и ничего кроме: снят запрет прямого шага — краснеют три («ПОДДЕЛКА ПРЯМАЯ», «ВСЕ ЧЕТЫРЕ ОБОСНОВАНИЯ», «гипотеза «дано»»); снято поле посылка.free — одна («ПОДДЕЛКА ИНДУКЦИЕЙ»); снят четвёртый связыватель у сторожа захвата — одна («ПОДДЕЛКА ЗАХВАТОМ»); возвращено ложное утверждение в витрину — одна («КЛАСС»), и в отказе стоят файл, имя, вердикт и контрпример.

Чего сторож не покрывает, и это надо сказать. Файл с ОТВЕРГНУТЫМ термом в корпус попасть не может: flang check его не пропустит, и свод требует нуля отвергнутых. А файл с ошибочно ПРИНЯТЫМ термом пропустится и в корпусе окажется — это ровно тот случай, ради которого сторож и написан. Сетка при этом конечна, и молчание сторожа доказательством не является — по той же причине, по какой им не является «сетка N» в самой ведомости. Сторож несимметричен нарочно: найденный контрпример окончателен, ненайденный не говорит ничего.

Слова ведомости: их стало пять

flang check --proof теперь различает:

• доказано — утверждение обо ВСЕХ входах: терм принят ядром (или завершение выведено анализом);
• доказано индукцией по «Т»: база N случаев, шаг при допущении на частях — то же самое и строго больше: носитель утверждения БЕСКОНЕЧЕН, и покрыт он не перечислением, а принципом, прочитанным с объявления суммы «Т». Слово пятое, а не оттенок четвёртого, и путать их нельзя ровно по той же причине, по которой нельзя путать «доказано» и «сетка»: первое говорит «цель свелась к названным фактам», второе — «цель верна на носителе, который нельзя перебрать».

Отличать его надо и от «доказано структурой» из раздела «чем несётся обещание „тотальная“»: там речь о ЗАВЕРШЕНИИ функции, здесь — об истинности утверждения о её результате. Одно без другого бывает сплошь и рядом: функция «Высота» была доказана структурой с самого начала, а «высота неотрицательна» стояло сеткой до этой работы;

• сетка N значений: нарушений не найдено — прогнано на N значениях автора и нарушений на них не нашлось; это НЕ доказательство. «Не найдено» означает здесь «ИСКАЛИ и не нашли», и это не подразумевается, а исполняется: примеры прогоняет flang/src/grid.mjs тем же вычислителем, каким работает flang test. Когда прогона не было или он не дошёл — сказано «нарушений НЕ ИСКАЛИ», теми же словами;
• НАРУШЕНО на примере «…» — прогон нашёл вход автора, на котором утверждение ЛОЖНО. Слово шестое, и оно не про степень уверенности, а про факт, поэтому в словаре вверху ведомости его нет. Оно бьёт «доказано» и «сетку» (при «доказано» расходятся не два мнения, а доказательство и факт — это ошибка ядра) и ДОБАВЛЯЕТСЯ к «отвергнуто ядром», где оба факта смотрят в одну сторону;
• объявлено, не доказано — утверждение высказано, доказательства при нём нет вовсе. Сюда попадает старая форма теорема и постусловие без теоремы и без примеров;
• на веру — не посчитано ничем.

Разница между двумя последними содержательная: «на веру» — допущение, которое считать НЕЧЕМ (изоморфизм без даёт); «объявлено, не доказано» — утверждение, которое считать есть чем, а никто не считал. Первое требует новой проверки, второе — доказательства от автора.

Слова «проверено» в ведомости нет и не будет: оно и есть то, которое читается двумя способами. Запрет держится тестом.

Что перешло из сетки в доказанное, поимённо и с числами

Свод по корпусу (flang/scripts/proof-ledger.mjs) до индукции и сегодня:

Столбец «стало» описывает ТОТ ШАГ, а не сегодняшнее дерево, и путать их нельзя: свод растёт каждый день, а таблица шага — запись о работе, которую сделали. Что свод говорит про дерево на 15 августа 2026, после второй волны сборки: высказано 28 утверждений, доказано ядром 26 (из них 8 индукцией по объявленной сумме и 18 сведением цели с телом, а внутри этих шестнадцати ровно 3 опираются на объявленный тип аргумента), сетка 1, объявлено-не-доказано 1, отвергнуто 0, нарушено 0, шагов в принятых термах 18. Числа эти руками не сверяются: они стоят равенствами в flang/test/proof.test.mjs и сличаются с прозой docs/overview.ru.md сторожем flang/scripts/count-guard.mjs.

Три из семи — о настоящих функциях корпуса, стоявших там задолго до слоя доказательства:

Первое, что надо сказать честно: доказательства лежат НЕ У ФУНКЦИЙ. Они лежат в flang/proof/examples/corpus-numtree.flang, corpus-tree.flang и corpus-depth.flang, а тела функций перенесены туда ДОСЛОВНО. Причина была такая: у девяти слов слоя доказательства нет продукции в flang/self/parser.flang, а flang/stdlib, flang/core, flang/examples/leetcode, flang/examples/measure и flang/self входят в корпус побайтовой неподвижной точки самоприменения ЦЕЛИКОМ. Напиши обеспечивает у библиотечной функции — и парсер на flang перестанет давать тот же AST, что эталон. Это было проверено падением: сначала утверждения написались прямо в библиотеке, flang/test/self-parser.test.mjs покраснел на побайтовой сверке, и работа откатилась туда, где ей место.

Эта причина СНЯТА, и держать её записанной значило бы запрещать сделанное. Продукции написаны все девять: восемь — 15 августа 2026, девятое (требует) — при слиянии work/trebuet. Записей в ПРОБЕЛЫ_РАЗБОРА у них нет ни одной, а ПРОБЕЛЫ_РАЗБОРА снимаются с таблицы лексера прогоном, а не пишутся по памяти: там одна строка, inMonad, и у неё причина другая. Правило «flang/stdlib не имеет права ими пользоваться» из запрета переделано в СЧЁТ (flang/test/proof-kernel.test.mjs): слово разрешено и обязано стоять ровно там, где вписано, — и flang/stdlib/numbers.flang, higher-order.flang, logic.flang, strings.flang в этом списке уже стоят. Запрещено одно слово, по свойству, и не за разбор, а потому что ядро отвергает его всегда.

Что держит эти три файла на месте сегодня — другое. Постусловие переезжает к функции даром: оно живёт полем функции и едет вместе с ней. ТЕОРЕМА не едет — её берёт сборка программы, а не чтение файла, — и перенос теорем к функциям есть отдельная работа со своим прогоном, а не следствие продукции.

Второе: дословность переноса проверяет машина, а не глаз. flang/test/proof-kernel.test.mjs сличает дерево разбора тела, подписи и объявления типа с файлом корпуса и краснеет на любом расхождении. Разойдись хоть что-нибудь — и «утверждение корпуса» стало бы утверждением о похожей функции. Тела при этом не тронуты ни на знак; единственная добавленная строка — пример базового случая у «Глубина», которого в оригинале нет (там примеры стоят у соседней функции).

Третье: сами постусловия написаны этой работой, и иначе быть не могло — слово обеспечивает появилось предыдущей работой, и в корпусе не было ни одного постусловия за её пределами. Поэтому «было» — это состояние С постусловием и БЕЗ теоремы, и оно измерено прогоном ведомости до того, как теоремы написались, а не восстановлено по памяти.

Сторож на будущее. Чтобы соблазн написать обеспечивает прямо в библиотеке не стоил следующему сорока минут полного прогона, в flang/test/proof-kernel.test.mjs стоит проверка: ни один файл корпуса самоприменения не употребляет слов доказательства.

Ещё два утверждения («штраф неотрицателен» светофора и «ступень неотрицательна» из four-words.flang) перешли с четвёртого слова на пятое: они и были доказаны, но теперь ведомость называет, ЧЕМ. Шестое — новое, в flang/proof/examples/stack.flang: «высота неотрицательна». Второе утверждение того же файла, «копия равна оригиналу», доказанным НЕ является и стоит сеткой одного примера — по причине, названной в самом файле и в таблице выше.

То же самое, шагом позже: начальная алгебра ВСТРОЕННОГО списка

Три новых — первые утверждения языка о встроенном списке, и все три о настоящих функциях библиотеки:

Второе и третье стоят здесь не для полноты. В lists.flang функций с двумя параметрами 19 из 28, и «второй параметр в заключении» — ровно то место, где правило по примеру до этой работы принимало ложь (см. «Граница честности»). Третье снимает подозрение, что функция-параметр индукции мешает: она проезжает посылку коэффициентом, как всякое поле не своего типа. Мешает она только тогда, когда заключение её УПОТРЕБЛЯЕТ, — у «Отобразить» и «Отфильтровать» так и есть, и они остались сеткой.

Число доказанных выросло на три, а число ПРИЧИН, по которым остальное не доказано, — с одной до трёх, и это второй результат той же работы. Раньше все пятнадцать утверждений о lists.flang стояли под одной строкой «начинать не с чего»; теперь 15 = 2 доказано + 8 (тело — свёртка или встроенная форма) + 4 (вид цели) + 1 (развёртка определения в базе).

Чего этой работой не сделано и почему. Шесть строк корпуса по-прежнему стоят сеткой с пределом — законы двух монад, изоморфизма, двух вложений и общей части (flang/examples/monad/order-total.flang, flang/examples/cat/*.flang). Индукция их не берёт, и это не недоделка, а другая задача: два закона монады из трёх квантифицированы по СТРЕЛКАМ Клейсли (то есть по функциям, а не по значениям), а правая единица и кругооборот изоморфизма упираются в посылку со связанными именами нерекурсивных полей — тот самый случай, который закроет упрощатель. Обещать их индукцией значило бы обещать не то.

И ещё одно, уже объявленным типом, — с числами

У всех девяти слов есть продукция в самоприменённом парсере (flang/self/parser.flang). Таблица ключевых слов в flang/self/lexer.flang их уже содержит — она сверяется с эталоном слово в слово, — и разбор к ним есть: восемь слов закрыты 15 августа 2026, девятое (требует) — при слиянии work/trebuet. Записи в ПРОБЕЛЫ_РАЗБОРА (flang/test/self-parser.test.mjs) у них нет ни одной, а сверка AST с эталоном идёт побайтово на всём каталоге.

Здесь стояло: «„Сколько дополнить“ лежит в flang/proof/examples/precondition.flang, а не в flang/stdlib/strings.flang, где ей место, потому что библиотека слов слоя доказательства употреблять не имеет права». Правдой это быть перестало: функция ПЕРЕЕХАЛА в библиотеку вместе со своим постусловием (work/stdlib-grow), и flang/stdlib/strings.flang:572 несёт обеспечивает «дополнение не выходит за точный потолок». Копия в precondition.flang осталась не долгом, а показом предусловия требует.

Свод по корпусу до этой работы и после (flang/scripts/proof-ledger.mjs):

Переехало утверждение о настоящей функции корпуса:

«Было» здесь — это состояние С постусловием и БЕЗ правки ядра, измеренное прогоном ведомости (сетка 3 по корпусу), а не восстановленное по памяти: тем же способом, каким мерилось «было» у трёх утверждений индукции выше.

Тело перенесено дословно в flang/proof/examples/corpus-natural.flang и сличается машиной — тем же тестом, что три прежних corpus-*.flang. Причина переноса та же и не новая: flang/examples/measure входит в корпус побайтовой неподвижной точки самоприменения целиком, и слово обеспечивает рядом с той функцией сломало бы сверку разборщика.

Долг, который эта работа сделала нагруженным: вход, лгущий про тип. Факт «первое не меньше 0» верен ровно настолько, насколько его проверяет типизатор. На границе flang run --args он не проверяется вовсе, и теперь это не гигиена, а дыра под доказанным утверждением:

$ flang run flang/examples/measure/natural.flang --function «Сумма пары» \
    --args '{"первое": -5, "второе": -5}'
{"function":"Сумма пары","args":{"первое":-5,"второе":-5},"result":-10}

$ … --args '{"первое": 2.5, "второе": 0.5}'
{"function":"Сумма пары","args":{"первое":2.5,"второе":0.5},"result":3}

Отрицательное и дробное объявлены нат и проходят молча; строка ловится, но не на границе, а внутри — на операции add, то есть по месту употребления, а не по объявлению. bindArguments в flang/bin/flang.mjs типов не читает ни одной строкой. Постусловие спасает только там, где оно написано: у flang/proof/examples/corpus-natural.flang тот же вход даёт честный отказ FLANG_PROPERTY, но это работа рантайма, а не проверка входа.

Чинится это НЕ в ядре: ядро обязано верить объявленному типу — иначе объявленный тип не значит ничего. Чинится на границе, сверкой --args с объявленными типами параметров.

Долг закрыт, и закрыт именно там, где назван: checkArguments сверяет вход с объявленным типом ДО вычисления (ветка work/entry-types-113, влита в сборку work/svodka вместе с этой). Ровно это и позволило отдать ядру вторую границу — см. следующий раздел.

И вторая граница того же объявления — потолок, с числами

Довод, по которому потолок вчера ядру НЕ отдали, стоял в reduce.mjs дословно: «факт, которым никто не пользуется, — это доверие, за которое никто не отвечает». Отвечающий появился (раздел выше), и потолок отдан. Правил сведения стало три; устройство правила, его доказательство о IEEE-754 и главная ловушка — в разделе 3б-кватер.

Свод по корпусу до этой работы и после (flang/scripts/proof-ledger.mjs):

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

«Было» здесь — состояние С постусловием и БЕЗ правки ядра, измеренное прогоном: диагностик 0, вердиктов ядра 0.

Тело перенесено дословно в flang/proof/examples/corpus-natural-ceiling.flang и сличается машиной — тем же тестом, что четыре прежних corpus-*.flang, и по той же причине: flang/examples/measure входит в неподвижную точку самоприменения целиком.

Долга эта работа не завела ни одного, и слов поверхности не прибавила ни одного. Утверждение записано восемью уже стоящими словами; число 2⁵³−1 написано в программе цифрами, потому что имён констант у языка нет, — но ядро сверяет цель не с этими цифрами, а с ТОЧНАЯ_СЕТКА.верх из types.mjs.

И третья граница той же подписи — ЦЕЛОСТЬ, с числами

Дно и потолок — это отрезок. Третье, что обещает точный тип и что ядро до сих пор не читало, — что значение ЦЕЛОЕ. Пока правил было три и все три про порядок, целость и правда была фактом, которым никто не пользуется. Появился случай, которому она нужна не для красоты, а иначе правило ЛОЖНО, — и она отдана.

Случай — ОСТАТОК, и он приехал вместе с точным десятичным типом (сотых, тысячных; flang/SPEC.md, раздел 3). Деньги на число не считаются, и это вычисление: 0.1 плюс 0.2 даёт 0.30000000000000004, а (0.1 плюс 0.2) плюс 0.3 и 0.1 плюс (0.2 плюс 0.3) дают 0.6000000000000001 и 0.6 — одно выражение в разном порядке даёт два ответа. сотых — целое число сотых долей, и на нём сложение снова ассоциативно.

Правило добавлено в ДВА уже стоявших, а не четвёртым:

`а остаток от Л` не меньше 0     при неотрицательном КОНЕЧНОМ `а` и Л ≠ 0
`а остаток от Л` не больше Л−1   при неотрицательном ЦЕЛОМ `а` и целом Л > 0

Почему это теорема о IEEE-754, а не удобство. Остаток вычисляется ТОЧНО — fmod не округляет, это часть стандарта, — равен а − trunc(а/Л)·Л и повторяет знак делимого. Отсюда обе строки. Обе посылки несут вес, и каждая проверена изъятием, а не обещанием:

• целость. 5.5 остаток от 2 равно 1.5, а 1.5 больше единицы. Сними факт целости — и вторая строка начнёт доказывать ложь о дробном входе;
• конечность. +∞ остаток от 100 — это NaN, а NaN не больше и не меньше ничего. Поэтому в список «конечное целое» НЕ входят сложение и умножение: в IEEE-754 1e308 плюс 1e308 даёт +∞, и посылка стала бы ложной ровно на переполнении;
• ненулевой делитель. а остаток от 0 — снова NaN, и «делитель не ноль» ядру взять неоткуда, кроме как из написанного числа. Имя типа нат нулём быть вправе, и потому именем делитель быть не может.

Свод по корпусу до этой работы и после (flang/scripts/proof-ledger.mjs):

И ЗАКОН, которого у число НЕТ

Одиннадцатый закон корпуса — моноид «Копейки»: носитель сотых, операция «Сложить копейки», единица 0. Сетка 5 значений, 125 троек, нарушений не найдено.

Тот же моноид, объявленный на число с долями рубля в сетке, не собирается:

FLANG_MONOID_ASSOC: моноид «Доли»: операция не ассоциативна:
  на 0.1, 0.1, 0.6 слева вышло 0.8, справа 0.7999999999999999

Это самое важное, что даёт точный тип сверх точности, и оно не рассказано, а ПРОВЕРЕНО: язык отличает тип, на котором моноид есть, от типа, на котором его нет, и отличает ОТКАЗОМ СБОРКИ. Обе половины стоят тестом (flang/test/decimal.test.mjs, «ЗАКОН: …»).

Что при этом остаётся сеткой и названо своим словом: ассоциативность и нейтральность проверены на 125 тройках, а не доказаны — правил о равенстве вычислений у ядра нет и быть не может. КОММУТАТИВНОСТИ язык не проверяет вовсе: её нет в объявлении моноида, и говорить, что она доказуема, было бы неправдой.

Дефект, вскрытый этой работой и починенный в ней же. носитель нат на совершенно исправной программе давал «носитель объявлен как неизвестный тип» — носитель брался из AST сырым и не проходил нормализацию, а имена уточнений (в отличие от число) ключевыми словами не являются и приезжают узлом named. Значит НИ ОДИН моноид над нат, целое, сотых или тысячных не собирался никогда. Чинится одной строкой — тем же normalizeType, каким читаются типы параметров.

Изъятие здесь чище некуда: тело то же самое, отличается ОДНО СЛОВО в подписи — сотых против число, — и слово «доказано» исчезает (flang/test/decimal.test.mjs, «ИЗЪЯТИЕ: та же функция над число теряет слово «доказано»»).

Аксиом по-прежнему ноль, слов поверхности не прибавилось ни одного. Охват ядра вырос ровно на одну функцию корпуса — она восемнадцатая в списке flang/test/corpus-claims.test.mjs и первая, пришедшая не от нат.

Долг, названный прямо, — и закрытый 15 августа 2026

Здесь стояло: у восьми слов нет продукции в самоприменённом парсере (flang/self/parser.flang). Продукция написана — все восемь разбираются четырьмя продукциями, AST сходится с эталоном побайтово, и flang/proof целиком входит теперь в корпус сверки разборщика. Запись оставлена не для памяти, а потому что ниже названа ЦЕНА этого долга, и цена — часть измерения.

Побайтовая неподвижная точка самоприменения не страдает и теперь, но говорится это уже о другом: в её корпусе (flang/stdlib, flang/core, flang/examples/leetcode, flang/examples/measure, flang/self) стоят СЕМЬ постусловий, и AST на них сходится с эталоном побайтово — это прогнано, а не предположено (flang/test/self-parser.test.mjs). Теорем там по-прежнему ноль, и это не забывчивость: теорему в этих каталогах никто с эталоном не сверял, а flang/proof в корпусе сверки стоит целиком. Счёт сторожит proof-kernel.test.mjs («корпус самоприменения употребляет ровно обеспечивает и ровно семь раз»), и краснеет он в обе стороны.

Этот долг оказался дороже, чем читался, и работа по индукции в него уперлась. Пока его не было видно, он читался как «доказательства просто лежат в другом каталоге». На деле он значит другое: ни одно утверждение о функции корпуса нельзя записать РЯДОМ С ФУНКЦИЕЙ, потому что библиотека и решённые задачи входят в неподвижную точку целиком. Три доказанных индукцией утверждения корпуса поэтому лежат в flang/proof/examples/corpus-*.flang с дословно перенесёнными телами, а не у самих функций. Проверено падением: написанные в библиотеке, они покраснили flang/test/self-parser.test.mjs на побайтовой сверке AST.

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

Для ПОСТУСЛОВИЯ это верно уже сегодня. Для ТЕОРЕМЫ — ещё нет, и разница здесь не в парсере (он разбирает и её), а в сверке: доказательств индукцией в каталогах неподвижной точки не стояло ни одного, значит и сверено там ничего не было. Пять corpus-*.flang с индукцией поэтому остаются на месте до отдельной работы, которая перенесёт туда теорему и прогонит побайтовую сверку целиком.

**У пятого (corpus-factorial.flang) причина ДРУГАЯ, и её надо назвать отдельно.** Его функция лежит не в корпусе неподвижной точки, а в flang/examples/rosetta/factorial.flang — образце сверки ЧЕТЫРЁХ ПОВЕРХНОСТЕЙ (flang/test/surfaces.test.mjs). Восьми слов доказательства у эсперантской и китайской поверхностей нет вовсе, поэтому утверждение, написанное по-русски и не написанное там, разломало бы сверку деревьев, которая и есть смысл тех файлов. Двойник той же функции в flang/examples/measure/natural.flang упирается уже в первую причину — неподвижную точку. То есть у одного и того же тела ДВА разных запрета, и оба сняты будут разными работами.

Закрыто: выражение постусловия типизируется

Здесь стоял долг, найденный этой же работой: flang/src/types.mjs не читал поле postconditions ни одной строкой, и обеспечивает «бессмыслица» результат плюс "строка" проходило flang check с ответом valid: true. Долг закрыт — checkPostconditions в types.mjs, — и та же программа отвечает теперь двумя диагностиками: правый операнд «add»: ожидался число, получен строка и постусловие «бессмыслица» даёт число, а постусловие обязано быть признаком.

Проверок две, и вторая не следует из первой: результат плюс 1 типизируется безупречно и не является утверждением ни о чём. Область видимости взята у вычислителя, а не выдумана: результат (точнее, bind постусловия) кладётся поверх параметров ровно так же, как это делает stepPost в interpret.mjs. Имя, связанное квантором для всех, тип получает из параметра — другого источника у него нет и быть не может.

Запись убрана по правилу flang/test/missing.test.mjs: у названной недостачи стоит программа-улика, и как только недостачи не стало, улика покраснела и потребовала убрать запись. Так и вышло.

Закрыто: дано сверяется по типу, постусловие отвечает за своё завершение

Здесь стояли два долга той же работы. Оба закрыты, и оба — программой, которая раньше проходила молча.

Переменная теоремы сверяется по ТИПУ, а не только по имени. дано свет: «Несуществующий» отвечало valid: true; теперь та же программа отвечает FLANG_PROOF_VAR_TYPE: теорема «штраф неотрицателен» вводит «свет» как «Несуществующий», а у функции «Штраф» этот параметр объявлен как «Светофор».

Закрыто это НЕ в типизаторе, и место стоит назвать. types.mjs узел theorem не читает ни одной строкой — теорему с функцией сводит obligations.mjs, по имени, и там же стояла ровно половина этой сверки: «у функции такого параметра нет». Вторая половина — тип — легла рядом с первой, потому что это одно сведение, а не два. Парсер строит переменную теоремы тем же parseParameter, что и параметр функции, и говорит об этом прямо: «переменная теоремы и параметр функции — одно и то же: имя с типом».

Сверка идёт с ПАРАМЕТРОМ, а не с объявлениями модуля, и это строго сильнее: дано свет: число при параметре свет: «Светофор» называет существующий тип и всё равно доказывает не о той функции. Тип параметра типизатор уже проверил на существование — совпасть с ним значит и существовать, и относиться к делу.

Постусловие вошло в анализ завершаемости. flang/src/totality.mjs поле postconditions не читал вовсе, и программа ниже отвечала valid: true:

функция «Вечная»
  принимает н: число
  возвращает признак
  если н не меньше 0 то «Вечная» от (н плюс 1) иначе да

тотальная функция «Ф»
  принимает н: число
  возвращает число
  обеспечивает «зовёт обычную» «Вечная» от результат
  н

Теперь она отвечает FLANG_NOT_TOTAL: тотальная функция «Ф» вызывает обычную функцию «Вечная» в постусловии «зовёт обычную»: обычная функция может не завершиться … Постусловие считается после каждого возврата, значит вызов из него — часть вызова «Ф», а не заметка рядом с ним. Место названо в САМОМ сообщении не для полноты: обеспечивает стоит НАД телом и читается как объявление, и автор, услышавший «вызывает обычную», пошёл бы искать вызов в тело и не нашёл бы его. На вызове из тела обе вставки пусты, и старые сообщения остались прежними знак в знак.

Правило взято то же, каким проверяется тело, и легло туда же, где уже обходится мера, — по тому же доводу, каким там обходится она: обещание, которое ВЫЧИСЛЯЕТСЯ, отвечает за своё вычисление наравне с телом. Область видимости взята у вычислителя, а не выдумана: bind кладётся поверх параметров так же, как stepPost кладёт результат поверх окружения вызова, а происхождение у него null — про только что построенное значение не известно ничего.

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

Изъятия показаны тестами: flang/test/totality.test.mjs («постусловие — тоже код…» и «постусловие обходится в области видимости вычислителя…») и flang/test/proof-kernel.test.mjs («„дано“ теоремы сверяется по ТИПУ…»).

~~Долг, оставшийся от той же работы: гипотеза дано не типизируется~~ — ЗАКРЫТ 16 августа 2026

**Закрыт на неслитой ветке work/tipizirovat-dano (5b68cbf), в этом дереве ещё стоит.** Там checkTypes получил последним проходом checkTheorems (эталон) и «Проверить теоремы» (близнец, flang/self/types.flang): гипотеза читается общим выводом типа в области видимости параметров ФУНКЦИИ, чьё постусловие теорема закрывает, и тип её обязан быть признак. Все три улики ниже там отвергнуты, корпус не сдвинулся (гипотез-утверждений в дереве 0 при 75 теоремах), аксиом по-прежнему ноль. Здесь всё написанное дальше — правда; сольётся ветка — раздел снимать целиком.

Закрыта одна форма слова дано — переменная дано <имя>: <тип>. Вторая форма, гипотеза дано <утверждение>, не типизировалась НИ ОДНОЙ СТРОКОЙ: слова theorems в types.mjs было ноль вхождений. Улика — три программы, и все три flang check принимал:

теорема «штраф неотрицателен»
  дано свет: «Светофор»
  дано свет плюс "строка"      → valid: true, диагностик 0
  дано 5                       → valid: true, диагностик 0
  дано "строка"                → valid: true, диагностик 0

Гипотеза ехала в обязательство полем hypotheses и доходила до ядра невычислимой: сложение варианта со строкой не даёт признака никогда, то есть допущение не является допущением. Ловилось у гипотезы только несвязанное имя, и ловил его разбор языка: область видимости проверялась, тип — ничем.

Чинится тем же способом, каким чинилось постусловие, и место названо было верно: obligations.mjs типов не читает и читать не должен, значит это types.mjs. Проход checkTheorems стоит последним в checkTypes, читает гипотезу общим inferExpr и требует от неё признак; отказ — тот же FLANG_TYPE, что у постусловия и предусловия. Ответ на те же три программы теперь: «теорема «штраф неотрицателен»: гипотеза даёт нат (строка, число), а гипотеза обязана быть признаком».

Среда — параметры ФУНКЦИИ, а не объявления самой теоремы. Это среда, в которой гипотеза действительно окажется: обязательство едет к ядру с vars = параметры функции. Читать объявления теоремы вторым источником значило бы получить два ответа на вопрос «какого типа здесь имя» и второе сообщение о том же изъяне — тип переменной теоремы сверяет с параметром obligations.mjs (FLANG_PROOF_VAR_TYPE), и сверяет строго. Связка результат кладётся поверх параметров тем же способом, что в постусловии: разбор языка держит это имя в области видимости всей теоремы, и отказать ему типизатором значило бы отвергнуть принятое разбором.

Обе стороны сделаны в один заход. Близнец flang/self/types.flang получил тот же проход («Проверить теоремы»), и сверка у него побайтовая: тот же код, тот же текст, то же место. Стережётся это СВОЕЙ программой, а не корпусом, и причина измерена: теорем в дифференциальном корпусе ноль — они живут в flang/proof, а тот в сверку не входит, — значит прохода у близнеца могло бы не быть вовсе, не покрасив ни одной проверки (flang/test/self-types.test.mjs, «гипотеза теоремы»). Изъятие проведено с обеих сторон порознь, и краснеет каждая своя половина.

Корпуса это не сдвинуло, и число тому есть: гипотез-утверждений в корпусе 0 при 75 теоремах и 26 записях дано имя: тип. Ведомость до и после одна — 142 высказано, 115 доказано ядром, 0 отвергнуто. Дыра была открыта, но ещё не эксплуатировалась; закрыта она до того, а не после.

Замер по корпусу: сколько дало ядру чтение объявленного типа

Работа, названная выше, отвечала на вопрос «умеет ли ядро». Следом задан второй, и он был не задан ни разу: сколько корпуса стало от этого доказуемым. Отвечать такое памятью нельзя, поэтому вопрос ИСПОЛНЕН — обходом всех 2800 функций корпуса, каждой подставили её тело на место результат и спросили у свести, сводится ли «результат не меньше 0». Обход стоит в flang/test/corpus-claims.test.mjs и краснеет, если ответ изменится.

Ответ: десять функций из 2800, и семь из них ПИСАТЬ БЫЛО НЕЛЬЗЯ. Не потому, что ядро их не берёт — берёт, — а потому, что они лежат в каталогах побайтовой неподвижной точки самоприменения: flang/self — пять, flang/examples/leetcode — одна, flang/examples/measure — одна. Там у слова обеспечивает не было продукции у парсера на flang. Это не граница ядра, это долг № 2 ниже, и он был измерен: он стоил семи утверждений.

Раскладка эта — не из головы, она печатается тем же обходом и сверяется в corpus-claims.test.mjs («охват: семь из десяти НАПИСАНЫ»): пять, одна и одна, а не «шесть и одна», как стояло в первом счёте этой работы, — там flang/examples/measure выпал, а flang/self вырос на его место.

Написаны поэтому сперва два, оба на настоящих функциях корпуса и на двух поверхностях одной и той же: «Значение цифры» из flang/examples/rosetta/roman-numerals.flang и «Value of a symbol» из …-english.flang.

Последняя строка тут — та самая улика, из-за которой строкой выше разведены два слова: утверждений без теоремы стало втрое больше, а объявленный тип как читался одним, так одним и остался.

Долг закрыт: семь отложенных утверждений написаны (15 августа 2026)

Продукция слоя доказательства в flang/self/parser.flang написана — и семь утверждений, названных выше поимённо, переехали К САМИМ ФУНКЦИЯМ. Копий больше не нужно: тело не переносится, сличать нечего, «доказано» относится к той самой функции по построению, а не по сверке двух деревьев разбора.

При сборке work/svodka к ним прибавились пять того же вида — из трёх влитых с origin слоёв близнеца:

Сетка и «объявлено, не доказано» не выросли ни на единицу, и это не совпадение: ни одно утверждение не переехало между строками, все семь добавлены новыми.

Свод СОБРАННОГО дерева (work/svodka, 15 августа 2026)

Таблицы выше — шаги отдельных веток, и «стало» в каждой означает «стало на той ветке». Собранное дерево считалось один раз и одной командой (node flang/scripts/proof-ledger.mjs); вот что она напечатала.

Шесть утверждений сверх девятнадцати ветки пришли не работой над ядром: одно — «разность пары не выходит за точный потолок» из work/proof-ceiling, пять — пределы сеток трёх влитых с origin слоёв близнеца (self/iso.flang, self/monoid.flang, self/monad.flang — два, self/sets.flang). Ядро берёт их по одной и той же причине: предел объявлен литералом. Сетка и «объявлено, не доказано» не тронуты и здесь.

Охват при этом остался тем же по существу и вырос по счёту: цель «результат не меньше 0» сводится у 15 функций из 3329, и все двенадцать, лежащие в корпусе неподвижной точки, теперь НАПИСАНЫ (flang/test/corpus-claims.test.mjs).

Цена перехода оказалась не нулевой, и назвать её надо. Постусловие в корпусе неподвижной точки сломало одну сверку — и сломало по делу: flang/self/types.flang не типизировал постусловие ВОВСЕ, а эталон типизирует (checkPostconditions). На чистом файле это не видно никогда — обе стороны говорят «диагностик нет». Видно стало на ПОРЧЕНОМ: у 013-roman-to-integer.flang число заменяется строкой, эталон говорит «левый операнд сравнения «gte» имеет тип строка», близнец молчал. Дыра закрыта пятью функциями в self/types.flang; подробности — flang/self/SPEC.md, «Постусловие типизируется с 15 августа 2026».

Чего этот переезд НЕ отменил. Четыре файла flang/proof/examples/corpus-*.flang остаются на месте, и три из них — по-прежнему единственный способ высказать своё: теорема с индукцией в корпус неподвижной точки не переносилась и с эталоном там побайтово не сверялась. Четвёртый (corpus-natural.flang) стал дословной копией утверждения, которое теперь стоит и у функции, — отсюда «факт дал объявленный тип» читается ДВАЖДЫ, а не один раз. Убирать копию — отдельная работа: на неё смотрит proof-kernel.test.mjs четырьмя проверками.

Узкое место названо числом, а не настроением. В корпусе нет НИ ОДНОГО поля варианта, объявленного нат, — значит declarations у посылок индукции, ради которых правился initial.mjs, сегодня не применяются к корпусу нигде. А нат-параметры стоят у функций, чьи тела ядру не по зубам: умножение («Факториал»), вызов («Фибоначчи»), длина и обращение к полю. Шесть таких случаев — правдивых утверждений, которых ядро не берёт, — стояли исполняемым списком в том же файле теста: у каждого проверяется и правда (на примерах автора), и отказ ядра (дословно, вхождением в why). Сегодня их пять: «Глубина дерева» вычеркнута развёрткой определения (раздел «И третье»), и причина у «Фибоначчи» переписана — «развёртки определений у ядра нет» стало неправдой, а строка осталась, потому что рекурсия там идёт по числу.

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

Починка исполняемая и стоит рядом со списком: из настоящего тела корпусной функции убирается РОВНО названная помеха, всё прочее остаётся знак в знак, и у ядра спрашивается ещё раз. «Факториал» от (н минус 1) заменяется на н — цель сводится, значит помеха не умножение. Снять из ядра случай mul — эта проверка краснеет первой.

Переписаны обе причины, и вычеркнуть по-прежнему нечего: оба утверждения правда, и оба ядру не по зубам. У «Факториала» мешает непрозрачный вызов (тот же класс, что «Фибоначчи»); у «Пропущено ячеек» старая причина называла две помехи разом, и вторая («поле объявлено число») ядру неподвластна вовсе — настоящая же помеха третья и прежде не называлась ни разу: итог.пропущено есть поле свёртки, и после нормализации на месте итог стоит свёртка, а не имя.

Почему обращение к полю записи фактом ПОКА не стало — и почему теперь это выбор, а не запрет. Заказ просил читать объявленный тип поля так же, как ядро читает тип аргумента и тип поля варианта. Мешало этому не reduce.mjs, а то, что за нат в поле ЗАПИСИ не отвечал никто: recordType в flang/src/types.mjs сверял тип поля через sameType — симметричное равенство ФОРМЫ, для которого нат, целое и число суть один и тот же IEEE-754 double, — тогда как соседнее место для поля ВАРИАНТА давно сверялось через годится. Список из десяти мест, переведённых на годится, назвал поле варианта и пропустил поле записи.

Дыра была измерена и ЗАКРЫТА. Измерение: запись «Ящик» с вес равным (0 минус 1) при вес: нат проходило без единой диагностики, и поле ОТМЫВАЛО значение — «Прямо» от ((запись «Ящик» с вес равным (0 минус 1)).вес) типизировалось, хотя «Прямо» принимает нат. Тем самым бился факт, который у ядра УЖЕ есть: постусловие стояло «доказано по объявленным типам аргументов… обо ВСЕХ входах», а прогон отказывал FLANG_PROPERTY. То есть дыра позволяла доказать ложь.

Правка — одно слово (sameType → годится в recordType), и цена её измерена на всём дереве, а не оценена: 183 файла .flang (stdlib, examples, core, self, proof, conc) дают от неё ровно ОДНУ диагностику, в flang/self/monoid.flang, где «номер»: нат принимал («сбор».«номер») плюс 1, а сумма двух нат натуральным быть не обязана. Починено объявлением поля («номер»: число), а не ядром: объявление теперь говорит то, что есть на деле.

Факта из поля записи у ядра по-прежнему нет, но причина сменилась с «нельзя» на «ещё не заведён»: отвечающий появился, и завести факт можно источником по образцу известноеПоТипу. Улика исполняемая и стоит на месте, только в положительной форме (proof-kernel.test.mjs, «ДЫРА ЗАКРЫТА: поле записи больше не отмывает значение»): она требует диагностики там, где раньше требовала её отсутствия, и краснеет, если факт заведут молча.

Из этого списка два случая — НЕ про правило сведения, и потому названы отдельно здесь. Оба про то, чем закрывается посылка.

И третье: развёртка определения, с числами

Свод по корпусу до этой работы и после (flang/scripts/proof-ledger.mjs):

Переехали два утверждения, и оба были названы уликами ЗАРАНЕЕ — одно владельцем языка, другое исполняемым заказом в flang/test/corpus-claims.test.mjs:

Второе — утверждение о настоящей функции корпуса, и «было» у него означает не «сетку», а пустоту: заказ прямо говорил, что ядро этого не берёт, и потому утверждение не писалось. Тела «Глубина дерева» и «Глубже» перенесены дословно, и сличаются машиной ОБА: тело «Глубже» вошло в доказательство развёрткой, значит расхождение с библиотекой означало бы доказательство о другой функции ровно так же, как расхождение в теле доказываемой.

Охват «результат не меньше 0» не изменился: как было десять функций из 2800, так и осталось десять из 2802. Это не разочарование, а измерение, и оно названо: развёртка помогает там, где утверждение доказывается ШАГОМ ИНДУКЦИИ, а обход охвата спрашивает ядро про постусловие БЕЗ теоремы — одной подстановкой тела. Развёртка при этом в обходе включена (иначе он мерил бы вчерашнее ядро), и у одной из десяти функций («Байтов у символа» в flang/self/emit-c.flang) она теперь и правда срабатывает — просто эта функция бралась и без неё.

Из-за этого же одна строка заказа была вычеркнута ЧЕЛОВЕКОМ, а не тестом, и об этом сказано в самом файле теста. Причина строки «Глубина дерева» была про шаг индукции, а проверка при ней — про постусловие без теоремы; вопрос и причина разошлись, и потому строка осталась бы зелёной после того, как ядро научилось. Список, который не умеет вычеркнуть себя сам, — это половина списка, и исправляется это не подновлением строки, а проверкой посылки принципа вместо тела функции.

Закрыто: базу посылки было нечем закрыть, кроме примера

Здесь стоял долг, и запись его была такой: «Глубина» из flang/examples/leetcode/104-maximum-depth-of-binary-tree.flang (и её близнец из 110-balanced-binary-tree.flang) доказывалась бы индукцией целиком — обе посылки СВОДЯТСЯ, — но написать теорему нельзя, потому что базу закрывать нечем: по предположению в базе отвергается по делу, а по примеру требует примера, которого у этой функции нет ни одного. Цена была измерена: две функции корпуса.

Долг закрыт ровно тем шагом, каким и был назван, и без нового слова поверхности. Покрытие означает теперь то, чем было с самого начала: о КАЖДОЙ посылке принципа сказано. Сказать может автор словом случай или ЯДРО — одним свести на посылку, без единого перебора, тем же путём, каким закрывается постусловие без теоремы (поОбъявленномуТипу).

Граница у правила одна, зато жёсткая: ядро закрывает посылку БЕЗ ЕДИНОГО ДОПУЩЕНИЯ ИНДУКЦИИ. Допущения в этот вызов свести не передаются вовсе — только объявления подписи и факты самого разбора. Довод не про осторожность, а про то, что такое доказательство индукцией: посылка, сведённая без допущений, индукции не потребовала (она того же рода, что постусловие без теоремы); посылка, сведённая ДОПУЩЕНИЕМ, — это шаг, и что он опёрся на допущение, обязан сказать автор словом по предположению. Разреши здесь допущения — теорема из одного случая доказывала бы всё подряд, а ведомость писала бы «шаг при допущении» о шаге, которого никто не писал. Проверено изъятием обеих сторон (flang/test/proof-kernel.test.mjs: «изъят ШАГ индукции» краснеет, «изъята БАЗА» зеленеет со словом by: reduction).

Что от этого стало в дереве. Из corpus-depth.flang УБРАН пример «У листа глубины нет» — единственная строка, которой в оригинале не было и которая дописывалась ради базы. Перенос стал дословным, и дословность сличается теперь и по примерам, а не только по телу с подписью. Обе функции корпуса, в которых цена долга была измерена, проверяются исполняемо: к тексту 104-… и 110-… дописываются РОВНО ДВЕ вещи — утверждение и теорема, — и ядро говорит «доказано индукцией по «Дерево»». На ядре до этой работы тот же файл отвергался кодом FLANG_PROOF_INDUCTION_CASES.

И вычеркнул строку заказа ТЕСТ, а не человек — в отличие от предыдущей вычеркнутой строки. Причина строки была про ПОСЫЛКУ ПРИНЦИПА, а проверка при ней спрашивала про постусловие БЕЗ теоремы; вопрос переписан на тот, про который причина.

Чего это НЕ закрыло. Тот же тупик с другой стороны — у варианта БЕЗ рекурсии, но С полями (вариант «Ответ» содержит код: число, тело: строка в flang/examples/web/orders-api.flang) — остался: посылка не замкнута, значит по примеру её не закроет; допущений у неё нет, значит и по предположению тоже; а свести её не закрывает, потому что в заключении живёт свободное имя поля. Закроет её упрощатель, как и было сказано.

Закрыто: «нарушений не найдено» стало означать «искали и не нашли»

Долг был записан здесь с уликой: ведомость печатала у сетки строку «сетка N значений (примеры функции): нарушений не найдено», а число N брала из obligations.mjs (grid: примеры.length) — то есть СЧИТАЛА примеры, а не прогоняла их. Порча на один знак (не меньше 0 → не меньше 1) давала два ответа об одном файле в одну секунду:

$ flang check flang/examples/rosetta/roman-numerals.flang --proof
  постусловие «значение цифры неотрицательно» … — сетка 3 значения
  (примеры функции): нарушений не найдено
$ flang test flang/examples/rosetta/roman-numerals.flang
  {"valid":false, … "example":"Не римская цифра — ноль","code":"FLANG_PROPERTY"}

Выбран был ПЕРВЫЙ путь из двух названных — сетка считается прогоном, — потому что второй («сказать, кто ищет, а кто считает») оставлял бы читателю число, которого ни один слой не проверил. Цена измерена и оказалась в шуме: обход всего корпуса node flang/scripts/proof-ledger.mjs — 2,54 с до и 2,51 с после, потому что сеток в корпусе двенадцать и в каждой не больше трёх примеров. Общая цена ограничена сверху ценой flang test для тех же функций: прогоняются только примеры функций, при которых написано постусловие.

Ищет flang/src/grid.mjs. Прогон идёт по программе-ТЕНИ, где оставлено ровно одно постусловие — то, о котором спрашивают, — и тогда отказ с его кодом принадлежит ему и никому больше; проверяются при этом ВСЕ возвраты функции, включая рекурсивные, потому что постусловие проверяет вычислитель, а не сам поиск. Пропустить то, что найдёт flang test, этот поиск поэтому не может.

Ответов три, и они не сливаются: «нарушений не найдено (искали прогоном на всех N)», «НАРУШЕНО на примере «…»» и «нарушений НЕ ИСКАЛИ». Третий сказан теми же словами нарочно: честное «не искали» допустимо, молчаливое «считаем, что всё хорошо» — нет.

Та же мерка, приложенная к соседним строкам свода

Строк в своде, говорящих «столько-то и ни одного больше», четыре. Проверены все четыре одним вопросом: получено ли число ПОИСКОМ.

Закон, нарушенный на сетке, попадал в отчёт строкой честного. monoid.mjs, monad.mjs и iso.mjs клали запись в checked безусловно, и ведомость печатала о моноиде с двумя диагностиками «сетка 5 значений (предел 12), 2 троек: нарушений не найдено». Программа при этом отказная и flang check ведомости не печатает — но proofLedger вывозится как функция, и отчёт по ней собирают инструменты. Списано устройство с sets.mjs, который нарушенное вложение в checked не клал с самого начала.

Хуже того — обрыв обхода, и он достижим у ЦЕЛОЙ программы. В monoid.mjs стоял голый break авария: операция отказала на тройке — обход прекращался без единой диагностики, а запись уходила такая же, как у пройденной насквозь сетки. Замер на фикстуре (proof.test.mjs, «оборванный обход сетки назван обрывом»): сетка 5 значений, обход оборвался на 11-й тройке из 125, а строка говорила «10 троек: нарушений не найдено». Это единственный из четырёх случаев, где соврать можно было прямо в выводе flang check --proof.

«Отвергнуто ядром: 0» было тавтологией. Отвергнутый терм — это отказ, у отказного файла ведомости нет, а свод складывал только ведомости: ноль означал «сюда такое не попадает», а читался как «искали и не нашли». Считается теперь и у файлов без ведомости; изъятие: испорченная теорема в corpus-numtree.flang даёт «отвергнуто ядром: 1» вместо прежнего нуля при тихо выпавшем файле.

Заказ от библиотеки: что меряет, чего не хватает

Здесь не пожелания, а замер по flang/stdlib — двенадцать модулей, 5080 строка, 185 функций. Замер стоит исполняемым тестом (flang/test/stdlib-claims.test.mjs), а каждый пункт заказа — настоящей функцией библиотеки, настоящей попыткой доказательства и настоящим кодом отказа. Появится названное — проверка ПОКРАСНЕЕТ и потребует перевести утверждение из сетки в доказанное.

Скольких функций индукция может коснуться сегодня: 55 из 208. Было 28. Чтобы ядро могло хотя бы начать, нужны две вещи, и обе читаются с объявлений: параметр, у типа которого ЕСТЬ начальная алгебра, и тело — разбор этого параметра на верхнем уровне. Параметр объявленной суммы есть у 35, разбор по нему — у 28: это число не сдвинулось и сдвинуться не должно было. Параметр-СПИСОК есть у 90, разбор по нему — у 27, и весь прирост оттуда.

У числа и признака конструкторов нет вовсе, множество — своя работа, а strings.flang получил ровно одну функцию, и ту за работу над списком, а не над строкой: строке алгебра не дана нарочно (раздел 3а-бис).

ДВА ПУНКТА ЗАЧЁРКНУТЫ, И ВТОРОЙ — НЕ ЭТОЙ РАБОТОЙ. Замер снимался на дереве ветки, а в собранном дереве развёртка определений уже была (work/kernel-unfold); при сборке work/svodka2 требования теста перевёрнуты с «обязано отвергнуться» на «обязано доказаться», потому что стеречь слабость ядра и краснеть на его усилении — это сторож наоборот. Сколько утверждений библиотеки от этого переехало из сетки в доказанное, здесь НЕ пересчитано: разложение ниже снято на дереве ветки, и числа в нём читать надо как её замер.

Первый пункт был качественно иным: остальные про силу правил, а он про то, что доказательства не с чего НАЧАТЬ. Он закрыт, и польза видна не только в числе доказанного: **раньше у всех пятнадцати утверждений о lists.flang причина была одна, теперь у каждого своя** — 15 = 2 доказано + 8 (тело — свёртка или встроенная форма) + 4 (цель сравнивает не с нулём и не на равенство) + 1 (базе не хватает развёртки определения). Разбор стоит исполняемым замером в flang/test/stdlib-claims.test.mjs.

Пункт про тело-свёртку оказался ровно таким дешёвым, как здесь и было сказано: свёртка — катаморфизм ТОЙ ЖЕ начальной алгебры, из которой читается принцип индукции (раздел 3а). Закрыт он 16 августа 2026 и закрыт не катаморфизмом в общем виде, а двумя посылками — началом и шагом (раздел 3б-секстэ): для цели «не меньше 0» этого хватает, а посылок с ветвей разбор брать не приходится вовсе. Из восьми утверждений о lists.flang, у которых тело не разбор, доказано одно; остальные семь упираются уже не в свёртку, а в цель другого вида.

Поиск доказательства: недоверенный оракул над ядром

Здесь стояло, и остаётся стоять: ядро ничего не ищет (раздел 3). Поиск появился не в ядре, а РЯДОМ с ним — flang/proof/search.mjs, — и граница между ними жёстче, чем между тремя слоями выше: оракул предлагает кандидата, ядро проверяет его ТЕМ ЖЕ кодом, каким проверяет написанное человеком.

Корректность поиска доказывать не нужно, и это не поблажка, а всё устройство. Он вправе быть перебором, эвристикой, чем угодно; соврёт, ошибётся или пошутит — ядро отвергнет. Ровно это и делает затею безопасной: в контур доверия оракул не входит ни одной строкой, и читать его целиком, чтобы поверить ведомости, не надо.

Улика ДО: сколько корпуса ждало ненаписанной цепочки

Число снято прогоном ДО всякой правки, и оно решало, стоит ли работа своей цены. Свод корпуса: высказано 53 утверждения, 33 доказано ядром, 20 не доказано. Сегодня это неправда — корпус с тех пор вырос, — и число оставлено надгробием того дня, а не сводом на сейчас: сегодняшний свод печатает flang/scripts/proof-ledger.mjs. Из этих двадцати ненаписанной цепочки не ждёт НИ ОДНО: каждое упирается в правила ядра, а не в автора, и это проверено вопросом к свести у каждой посылки принципа:

Раскладка печатается той же командой, что и всё остальное (node flang/scripts/proof-search.mjs), а не пересказывается по памяти.

Отсюда честный вывод, который стоит сказать прямо: сегодня поиск не прибавляет к ведомости ни одного «доказано», и ведомость до этой работы и после совпадает знак в знак. Прибавит он в тот день, когда у ядра появится новое правило, — и тогда ему не понадобится, чтобы кто-то писал цепочки руками.

Второе число: ПЕРЕВЫВОД — 11 из 11

«Нашёл 0 нового» само по себе не говорит, работает ли поиск вообще, поэтому считается и обратное. У каждого доказательства индукцией, написанного в корпусе РУКОЙ, теорема снимается из исходника, и оракул ищет её заново. Их одиннадцать, и все одиннадцать он находит сам — перечисление «Светофора» (три случая, все примером), объявленные суммы, ВСТРОЕННЫЙ список и цель-равенство «копия равна оригиналу». Считает это node flang/scripts/proof-search.mjs, и находкой считается только вердикт ведомости, а не мнение оракула.

То есть работа снимает не недоказанность, а РУЧНУЮ РАБОТУ: для класса, который ядро уже умеет, цепочку писать больше не надо.

Устройство: перебор в глубину по случаям, два названных предела

Спуск идёт по СЛУЧАЯМ индукции: уровень — случай, ветка — обоснование. Отсекает не эвристика оракула, а само ядро: у вердикта есть вердикт каждого случая порознь (проверитьИндукцию, поле cases), и спуск читает его. Поэтому перебор из степенного становится линейным, а принимает по-прежнему ядро и принимает кандидата ЦЕЛИКОМ.

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

Пределов два, и оба печатаются в отказе, когда упёрлись, — тем же приёмом, каким говорит о себе ПРЕДЕЛ_РАЗВЁРТКИ:

Ни то, ни другое число НЕ про состоятельность: оракул ничего не доказывает, поэтому остановиться раньше — значит найти МЕНЬШЕ, а не найти ложное. «Не нашёл» и «не искал дальше» — разные ответы, и отказ их различает.

Цепочка внутри случая длиной в один шаг, и это решение: сегодня ни одно правило не читает списка известно (proofterm.mjs, проверитьЦепочку), значит второй шаг мог бы только ослабить вердикт. Появится правило, которое известно читает, — здесь придётся завести третий предел, и это будет решение, а не случайность.

Находка — ТЕКСТ на языке, а не дерево, и это вторая половина недоверия

Оракул мог бы отдавать ядру готовый узел AST. Он отдаёт СТРОКИ теми же восемью словами, какими доказательство пишет человек, и текст проезжает ОБЫЧНЫЙ разборщик и ОБЫЧНЫЙ слой обязательств. Там стоят проверки, которых у ядра нет: утверждение теоремы обязано совпасть с постусловием слово в слово (FLANG_PROOF_CLAIM_MISMATCH), переменная — с параметром по имени И типу (FLANG_PROOF_VAR_TYPE). Отдай оракул дерево — эти проверки остались бы у него внутри, то есть их не было бы.

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

Изъятие: ядро не верит оракулу ни на грамм

Свойство, ради которого всё это безопасно, нельзя показать на честном оракуле: зелёный цвет означал бы только, что оба согласны. Поэтому у оракула есть рубильник ЛГАТЬ, и он не для отладки. Изъятий три, и все три стоят проверками в flang/test/proof-search.test.mjs:

Проверяется не только отказ, но и то, что доказанность не прибавилась ни на единицу: у файла бывают и другие утверждения, и считать их за находку ложного кандидата значило бы мерить не то. Мерка снимается с того же файла БЕЗ всякой теоремы, и прирост обязан быть ровно один и ровно от честной находки.

Портится при этом НАЙДЕННОЕ, а не поиск: подмени шаг раньше — и перебор просто не нашёл бы ничего, то есть изъятие показывало бы не то.

Поиск не обязателен, и это держится не обещанием

Ведомость от оракула не меняется, потому что его никто не зовёт: ни ядро, ни flang check, ни печать. Это проверяется чтением исходников — появись import … search.mjs в рабочем пути языка, проверка покраснеет и потребует объяснить, зачем поиск попал в контур. «Доказано» в flang check --proof означает «доказательство написано в файле и принято ядром», а не «инструмент сумел бы его написать».

Найденное поэтому печатается текстом, который человек впишет в файл сам (или впишет node flang/scripts/proof-search.mjs --write <файл>), а не подставляется за него молча.

Граница, названная прямо: поиск пишет на ОДНОЙ поверхности

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

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

Чего эта работа не отменила

Прежняя запись «тактик нет и не будет» (раздел 1) остаётся верной знак в знак, и путать её с этим разделом нельзя. Тактика — метапрограмма на самом языке, ворочающая состояние цели; её не написать, потому что в flang всё либо тотально, либо объявлено обычным. Оракул — не тактика: он не часть языка, живёт вне его, а на выходе даёт не состояние цели, а ТЕКСТ доказательства, который язык разбирает обычным разборщиком. Долг поверхности от него не вырос ни на слово: ни одного нового ключевого слова не заведено.

Что дальше

1. ~~**Типизировать гипотезу дано — долг выше, он первый.~~ Сделано 16 августа 2026** и слито в это дерево (ветка work/tipizirovat-dano, 5b68cbf): проход checkTheorems стоит последним в checkTypes у эталона (flang/src/types.mjs), «Проверить теоремы» — у близнеца (flang/self/types.flang); гипотеза читается общим выводом типа, тип обязан быть признак, отказ — тот же FLANG_TYPE, что у постусловия и предусловия. Улика: три программы, дававшие valid: true на невычислимой гипотезе, отвергнуты. Корпус не сдвинулся: гипотез-утверждений в нём 0 при 75 теоремах — дыра закрыта до того, как её начали использовать, а не после; аксиом по-прежнему ноль.
2. ~~**Аксиомы арифметики над нат — закрывает рекурсивный случай.~~ Сделано иначе, и это стоит сказать прямо.** Рекурсивный случай закрыт без единой аксиомы: вместо того чтобы принять на веру факты порядка, ядро получило ТРИ ПРАВИЛА СВЕДЕНИЯ, каждое из которых — доказанная теорема о IEEE-754 (раздел 3в). Точный тип нат от этого нужен не меньше, но нужен он теперь для ДРУГОГО: для утверждений вида «х минус 1 меньше х», которые на IEEE-754 ложны и правилом стать не могут никогда.

1-бис. ~~**Проверять --args по объявленным типам~~ — закрыто** на ветке work/entry-types-113 (checkArguments зовётся до вычисления). Это и был отвечающий, которого не хватало потолку: пока его не было, ядро читало у нат только дно. Теперь читает обе границы (раздел 3б-кватер).

1. ~~Продукция в самоприменённом парсере — закрывает долг выше.~~ Сделано 15 августа 2026, и долг оплачен полностью: семь отложенных утверждений написаны у самих функций. Осталась ПОЛОВИНА того же пути — перенести к функциям теорему с индукцией и прогнать на ней побайтовую сверку; пока этого нет, пять corpus-*.flang стоят на месте, а восьмое слово обеспечивает в этих каталогах ловит сторож в proof-kernel.test.mjs. Ни индукция, ни объявленный тип, ни его потолок, ни развёртка определения долга не увеличили: новых слов поверхности не заведено ни одного, и всё работает восемью уже стоящими. Развёртка не потребовала девятого слова намеренно: она не обоснование шага, а переписка нормализации, и назвать её словом значило бы дать автору распоряжаться тем, чем распоряжается правило.

2-бис. Первая половина сделана: у поля записи появился отвечающий. recordType в flang/src/types.mjs сверяет поле через годится, а не через sameType, и поле больше не ОТМЫВАЕТ значение (раздел «Узкое место»). Цена измерена на всём дереве: одна диагностика из 183 файлов, в flang/self/monoid.flang, и та по делу — «номер»: нат принимал сумму двух нат; поле объявлено число. Осталась вторая половина: завести ядру факт — объявленный тип поля наравне с типом аргумента и типом поля варианта, источником по образцу известноеПоТипу, а не новым решающим правилом. Стережёт это исполняемая улика в proof-kernel.test.mjs («ДЫРА ЗАКРЫТА»): заведут факт молча — она покраснеет.

1. Сличение по вызову — по свойству «…» сегодня отвергается, когда надо свести результат шага с результатом другой функции. Это не поиск, а чтение подстановки с узла вызова, и делается тем же приёмом. Развёртка определения (раздел 3б-бис) этого не закрыла, и путать их нельзя: развёртка читает ТЕЛО чужой функции, по свойству — её ОБЕЩАНИЕ. Там, где тело разворачивать нельзя (рекурсия по числу, чужой модуль, нат без конструкторов), обещание остаётся единственным, на что можно опереться. С этого дня у пункта есть вторая половина выгоды: по свойству войдёт в закрытый список обоснований поиска (раздел «Поиск доказательства»), и цепочки с ним никому не придётся писать руками.
2. Упрощатель — условная переписка с проверкой завершаемости самой переписки (устройство подсмотреть у Isabelle). Ею ядро будет проверять коммутацию диаграмм: доказательство равенства становится коммутирующей диаграммой, и ядро проверяет коммутацию перепиской. Нормализация из reduce.mjs — её первый и самый узкий кусок: четыре переписки, из них одна — развёртка определения под четырьмя названными ограничителями. Именно упрощатель закроет посылку с непрозрачными полями без частей (случай «Есть» содержит значение: «А»), а вместе с ней — законы монады и изоморфизма, которые сегодня стоят в ведомости сеткой 6 и 2 значений.
3. Решатель для линейной арифметики — обязательства для него уже лежат данными, ему останется их прочитать.
4. ~~Заключение посылки для тела-свёртки~~ — СДЕЛАНО 16 августа 2026 (раздел 3б-секстэ), и сделано не так, как здесь предполагалось. Строить заключение посылки не понадобилось вовсе: у свёртки есть начало и шаг, и для цели «не меньше 0» это и есть две посылки индукции по списку. Охват по корпусу вырос с 17 функций до 43 — вместе со вторым правилом того же дня (результат встроенной формы), и цена каждого измерена изъятием порознь. ЧТО ОСТАЛОСЬ ОТ ПУНКТА: цель, сравнивающая НЕ С НУЛЁМ («не длиннее исходного», «равно длине»), — но это уже пункт про правила сведения, а не про свёртку: тело её ядро теперь читает.
5. Начальная алгебра строки — 19 функций strings.flang, из них индукции доступна одна, и та за работу над списком. Работа не в том, чтобы повторить список: функтор у строки другой, потому что голова строки — тоже строка, и правило «поле того же типа» назовёт местом X оба поля. Нужен либо отдельный довод, почему местом X считать только хвост, либо тип символа — а он тянет за собой изменение всей поверхности.
6. **Обоснования поиска: по свойству и цепочка длиннее одного шага.** Оба ждут не поиска, а ядра: первое — сличения по вызову (пункт 3), второе — правила, которое читает список известно. Пункт стоит здесь, чтобы усиление ядра сразу считалось и на этой стороне: сегодня поиск не находит по корпусу ни одного нового доказательства (раздел «Поиск доказательства»), и ноль этот стоит исполняемой проверкой, которая покраснеет в тот же день.

Чем эти пункты отличаются от закрытого первого. Все они про силу правил; первый был про то, что доказательства не с чего НАЧАТЬ. Разница видна числом: он один сдвинул «доказано ядром» с 6 на 9 и «доступно индукции» с 28 функций библиотеки на 50, не прибавив к ядру ни одной аксиомы и ни одного нового правила сведения — только чтение объявления, которое у языка уже было.

1. Шире прочитать спуск по числу. Принцип по отрезку (раздел 3г) читает ровно одну форму спуска — н минус 1 — и пять форм условия дна. Список закрыт не по лени: каждая новая форма обязана приехать с рассуждением о IEEE-754 и о том, что цепочка спуска дна не проскакивает. Ближайшие честные кандидаты видны на корпусе: н минус 2 при дне н не больше 1 («Через два» из flang/examples/measure/natural.flang) законен, но требует посылки «шаг вниз не больше, чем ширина дна плюс единица», и написать её надо доказательством, а не удобством. То же про меру, отличную от самой переменной: сверять её с аргументом вызова ядру сегодня нечем, и сделать вид, что сверило, — хуже, чем отказать.
2. Условная форма утверждения. Ровно на неё упирается строка заказа «Фибоначчи», и упирается она НЕ в индукцию: у самой «Фибоначчи» тело — вызов, а не если, а лемма о «Фибоначчи шагом» была НЕПРЕДСТАВИМА, потому что «результат не меньше 0» о ней ложь (накопитель объявлен число). Верна там условная форма — «если накопители неотрицательны», — и записать её стало чем: слово требует приехало 16 августа 2026, лемма записана двумя предусловиями, и невысказываемой она быть перестала. Недоказанной осталась: теоремы при ней не написано, и ведомость честно говорит «сетка». Разницу между «недоказуемо» и «невысказываемо» путать по-прежнему нельзя — просто теперь это про другое.