fix(checker): replay property steps, cite across files, project fields

.github/workflows/binary.yml

@@ -340,8 +340,8 @@ jobs:
       # Примеры двух каталогов, которые СХОДЯТСЯ ЦЕЛИКОМ и потому годятся в
       # дешёвый гейт по голому коду возврата, без ведомости:
       #
-      #   flang/stdlib   51 файлов, 3745 примера, прошли все  44 мин
-      #   СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51
+      #   flang/stdlib   52 файлов, 3745 примера, прошли все  44 мин
+      #   СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52
       #   СНЯТО 2026-09-13 примеров-в flang/stdlib/*.flang = 3745
       #   flang/core      4 файла,  184 примера,  прошли все     15 с
       #   СНЯТО 2026-09-05 файлов flang/core/*.flang = 4

.github/workflows/ci.yml

@@ -164,8 +164,8 @@ permissions:
 
 jobs:
   # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c`
-  # планом на flang — 1052 файл; разбор в задаче 5821.
-  # СНЯТО 2026-09-17 файлов *.flang = 1052
+  # планом на flang — 1081 файл; разбор в задаче 5821.
+  # СНЯТО 2026-09-17 файлов *.flang = 1081
   #
   # Первой она стоит потому, что нарушение этого правила обесценивает ВСЕ
   # остальные работы разом. 24 августа 2026 имя типа «неотрицательное» ввели в

docs/README.ru.md

@@ -143,9 +143,9 @@ docs/tasks/     открытая и закрытая работа дерева,
 Внутри `flang/`: [`flang/self/`](../flang/self) — компилятор, 64 файла на flang —
 <!-- СНЯТО 2026-09-17 файлов flang/self/*.flang = 64 -->
 лексер, разбор, типы, завершаемость, ядро доказательств и по печати на каждую цель.
-[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **51 модуль, 1764 функции и 3745
+[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **52 модуль, 1764 функции и 3745
 примеров**, которые прогоняются при каждой проверке:
-<!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 -->
+<!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 -->
 <!-- СНЯТО 2026-09-13 примеров-в flang/stdlib/*.flang = 3745 -->
 списки, строки, числа, множества, словари, JSON, UTF-8, даты, два драйвера баз данных
 (`postgres`, `sqlite`), сеть (`http`, `tls`, `redis`), криптография, написанная на flang (`aes`,

docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md

@@ -192,7 +192,7 @@ flang check --proof --строго monoid.flang
   «Е не больше Е» не теорема, почему `0 × ∞` даёт не число, почему переставлять
   через скобки нельзя. Эти доводы не украшение: на них стоят посылки правил.
 - **Независимая проверяющая программа** — `flang/proof/checker/checker.c`,
-  10122 строк. <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10122 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
+  10257 строк. <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10257 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
   Она переигрывает записи и о новом виде значения не знает ничего.
 
 **И встречное число, которое меняет разговор о втором варианте.** Тип `целое`

docs/course/11-boundaries.md

@@ -66,8 +66,8 @@ draft: false
 **Полноценной сети нет.** Ходить в сеть язык умеет — есть поручения «Запросить»,
 «Открыть соединение», «Принять соединение», — но это примитивы, а не библиотека.
 
-**Библиотека невелика:** 51 файл, 32 074 строки
-<!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 --><!-- СНЯТО 2026-09-13 строк-в flang/stdlib/*.flang = 32074 -->
+**Библиотека невелика:** 52 файла, 32 091 строки
+<!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 --><!-- СНЯТО 2026-09-17 строк-в flang/stdlib/*.flang = 32091 -->
 (`ls flang/stdlib/*.flang | wc -l`, `cat flang/stdlib/*.flang | wc -l`,
 10 сентября 2026). Есть списки, строки, числа, словари, деревья, множества, JSON,
 HTTP-разбор, SHA-256, Base64, UTF-8, дата и время, функции высшего порядка.

docs/course/README.md

@@ -171,8 +171,8 @@ docs/course/check.flang: проверено — разбор, типы, заве
 | размеры напечатанного в восемь целей | `flang emit … --target …`, восемь прогонов подряд; байты — из собственной расшифровки `emit` |
 | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `cc`/`g++` 15.2.0, go 1.26.5, rustc 1.97.1, javac 26-internal, Elixir 1.20.3 на Erlang/OTP 29, node 26.7.0, Python 3.14.4, .NET 10.0.110 |
 | 82 задачи LeetCode, десятка самых коротких | `ls`, `wc -l`, счёт строк `пример` |
-| 51 файлов и 32 074 строки библиотеки <!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 --><!-- СНЯТО 2026-09-13 строк-в flang/stdlib/*.flang = 32074 --> | `ls flang/stdlib/*.flang`, `cat … \| wc -l` |
-| 724 заметки, 238 примеров, 384 файл доказательств <!-- СНЯТО 2026-09-17 файлов docs/zettel/*.md = 724 --><!-- СНЯТО 2026-09-17 файлов docs/examples/*.flang = 238 --><!-- СНЯТО 2026-09-17 файлов flang/proof/*.flang = 384 (задача 5502: проба пустой ведомости flang/proof/probes/strict/programs/no-obligations.flang; до неё 320, снято 2026-09-17) --> | `ls`, `find` |
+| 52 файлов и 32 091 строки библиотеки <!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 --><!-- СНЯТО 2026-09-17 строк-в flang/stdlib/*.flang = 32091 --> | `ls flang/stdlib/*.flang`, `cat … \| wc -l` |
+| 724 заметки, 238 примеров, 412 файл доказательств <!-- СНЯТО 2026-09-17 файлов docs/zettel/*.md = 724 --><!-- СНЯТО 2026-09-17 файлов docs/examples/*.flang = 238 --><!-- СНЯТО 2026-09-17 файлов flang/proof/*.flang = 412 (задача 5502: проба пустой ведомости flang/proof/probes/strict/programs/no-obligations.flang; до неё 320, снято 2026-09-17) --> | `ls`, `find` |
 | 2 из 20 — цена доказательств | `docs/benchmark-proof-cost-2.md`, замер 16 августа |
 
 **Чего переснять не удалось, и это надо знать.**

docs/design/nositel-tochnogo-celogo.md

@@ -441,7 +441,7 @@ flang check n-zapis-v-chislo.flang
    первая правка, и назвать её сейчас, не написав, значило бы выдумать.
 2. **Цену принуждения канона.** Сколько стоит запретить литерал-список в позиции нового
    типа — не мерил: это решение задачи 1412, а не замер.
-3. **Цену для проверяющей программы.** `checker.c` (10122 строк) <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10122 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
+3. **Цену для проверяющей программы.** `checker.c` (10257 строк) <!-- СНЯТО 2026-09-17 строк flang/proof/checker/checker.c = 10257 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
    о новом типе не знает ничего, и бюджет ему ADR-0035 §7 оценил в +150…+250 строк кода по
    образцу ADR-0029. Это оценка, и моя записка её не улучшает.
 4. **Скорость того же в рантайме.** Все числа §5 — арифметика, написанная НА ЯЗЫКЕ.

docs/flang/proof/checker/README.md

@@ -145,6 +145,36 @@ bootstrap/flang run-script trust:ceiling
     каждое `требует` «Г» из этого же исходника) обязано быть столько же, сколько
     блоков, и ни одно не записано дважды.
 
+18. **Шаг автора `по свойству` постусловия проверяется по существу, а не
+    привязкой.** Привязка `свойство строка N` обязана указывать на первое
+    объявление имени в модуле, но одной её мало: сверщик сам находит в теле
+    функции вызов той функции, которой принадлежит постусловие, строит его
+    инстанцию (те же проверки, что у хода «факт по свойству»: ребро, арность,
+    захват имён, оплата `требует` вызванной) и замыкает ею цель — модус-поненсом,
+    под охраной `если У то … иначе да` той же охраной, либо неотрицательностью по
+    построению, где инстанция стоит среди известного. Замкнуть не удалось — шаг
+    остаётся на слове ядра с названной причиной; вывод сверщик не выдумывает.
+    Постусловие, объявленное с ограничением `таких что`, фактом не берётся.
+19. **Свойство из другого файла.** Имя, которого нет в этом исходнике, ищется в
+    поданном наборе (`--зависимость ИСХОДНИК ЗАПИСЬ`): годится ровно одно
+    объявление, его модуль ввезён словом `использует` (самим файлом или кем-то из
+    набора), каждое имя в тексте свойства объявлено в том же модуле, видно по
+    спискам `только` и не совпадает с именем, объявленным здесь. Запись модуля
+    сверщик перепроверяет сам, тем же приёмом и с тем же набором, и берёт из неё
+    только проверенное по существу. Шаг и ход «факт по свойству … подстановка»
+    читают заголовок, связывания и ограничения утверждения из исходника модуля.
+    Без набора имя из другого файла — «не берусь», а не «не сошлось».
+20. **Поле результата и поле довода в узле тождества.** `результат.поле` —
+    это поле построенного значения, когда тело ветви — конструктор; `довод.поле`
+    под образцом случая — имя, связанное на этом поле. Допущение индукции
+    берётся только по полю того же типа, что и разбираемое значение.
+
+21. **Свободное утверждение «Т не меньше 0».** Утверждение без функции, чья цель
+    не говорит о `результат`, проигрывается той же грамматикой неотрицательности,
+    что тело функции: литерал, `длина`, сумма, произведение на положительный
+    литерал. Неотрицательным по объявлению считается только имя, связанное `для
+    всех` типом-отрезком (`неотрицательное`); ограничение `таких что` дна не даёт.
+
 Сверх того: **ни одной непрочитанной строки**. Строка записи, вид которой
 чекеру не известен, — отказ, а не «ладно». Мутационная проба (3000 порченых
 записей, зерно 7) показала, что порча полей `вид`, `конец утверждения` и полей

docs/fspec/clarifications.md

@@ -102,8 +102,8 @@ FLANG_EXAMPLE: пример «с промо — тридцать процент
 ## Перепись по библиотеке — замер 8 сентября 2026
 
 Замер устарел и здесь стоит как запись о прошлом: тогда мастер прогнали по
-`flang/stdlib/`, сегодня там 51 файл
-<!-- СНЯТО 2026-09-18 файлов flang/stdlib/*.flang = 51 -->, то есть перепись
+`flang/stdlib/`, сегодня там 52 файл
+<!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 -->, то есть перепись
 покрывает часть каталога, а не весь.
 
 Померено 18 файлов. Восемь померить не удалось, и мастер сказал об этом

docs/repository-layout.md

@@ -32,9 +32,9 @@ docs/tasks/     the open and closed work of the tree, one file per task
 Inside `flang/`: [`flang/self/`](../flang/self) is the compiler, 64 files of flang —
 <!-- СНЯТО 2026-09-17 файлов flang/self/*.flang = 64 -->
 lexer, parser, types, totality, proof kernel and one printer per target.
-[`flang/stdlib/`](../flang/stdlib) is the standard library — **51 modules, 1764 functions and 3745
+[`flang/stdlib/`](../flang/stdlib) is the standard library — **52 modules, 1764 functions and 3745
 examples** that run on every check:
-<!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 -->
+<!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 -->
 <!-- СНЯТО 2026-09-13 примеров-в flang/stdlib/*.flang = 3745 -->
 lists, strings, numbers, sets, maps, JSON, UTF-8, dates, two database drivers (`postgres`,
 `sqlite`), networking (`http`, `tls`, `redis`), a cryptography set written in flang (`aes`,

docs/repository-layout.ru.md

@@ -31,9 +31,9 @@ docs/tasks/     открытая и закрытая работа дерева,
 Внутри `flang/`: [`flang/self/`](../flang/self) — компилятор, 64 файлов на flang —
 <!-- СНЯТО 2026-09-17 файлов flang/self/*.flang = 64 -->
 лексер, разбор, типы, завершаемость, ядро доказательств и по печати на каждую цель.
-[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **51 модуль, 1764 функции и 3745
+[`flang/stdlib/`](../flang/stdlib) — стандартная библиотека: **52 модуль, 1764 функции и 3745
 примеров**, которые прогоняются при каждой проверке:
-<!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 -->
+<!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 -->
 <!-- СНЯТО 2026-09-13 примеров-в flang/stdlib/*.flang = 3745 -->
 списки, строки, числа, множества, словари, JSON, UTF-8, даты, два драйвера баз данных
 (`postgres`, `sqlite`), сеть (`http`, `tls`, `redis`), криптография, написанная на flang (`aes`,

docs/road-to-1-0.md

@@ -155,7 +155,7 @@ Homebrew с тем, что собрал сам конвейер выпуска;
 ## 6. Полноценная история пакетов и модулей
 
 **Что уже есть.** `scripts/registry-example/` — образец описания пакета.
-`flang/stdlib` — <!-- СНЯТО 2026-09-13 файлов flang/stdlib/*.flang = 51 --> 51 файл, <!-- СНЯТО 2026-09-13 строк-в flang/stdlib/*.flang = 32074 --> 32 074 строки.
+`flang/stdlib` — <!-- СНЯТО 2026-09-17 файлов flang/stdlib/*.flang = 52 --> 52 файла, <!-- СНЯТО 2026-09-17 строк-в flang/stdlib/*.flang = 32091 --> 32 091 строки.
 
 **Чего нет.** Почти всего: установки, разрешения версий, замыкания зависимостей.
 

docs/site/index.md

@@ -143,7 +143,7 @@ recounted on every push by `sh scripts/guards/published-vs-tree.sh --числа`
 steps: `дано` (given), `утверждаем` (we claim), `затем … по свойству «…»` (then …
 by property …), `индукция по …` (induction on …), `следовательно доказано`
 (hence proved). It reads like a proof in Isabelle's Isar, not like a script of
-tactics. There are **288** such theorems in the repository, 55 of them in the
+tactics. There are **303** such theorems in the repository, 55 of them in the
 standard library (`grep -rac '^\s*теорема ' flang --include='*.flang'`, summed
 with `awk`).
 

docs/site/index.ru.md

@@ -141,7 +141,7 @@ bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000
 **Доказательство руками можно писать и здесь.** `теорема` пишется по шагам:
 `дано`, `утверждаем`, `затем … по свойству «…»`, `индукция по …`,
 `следовательно доказано`. Это читается как доказательство на Isar из Isabelle, а
-не как скрипт из тактик. Таких теорем в дереве языка **288**, из них **55** в
+не как скрипт из тактик. Таких теорем в дереве языка **303**, из них **55** в
 стандартной библиотеке (`grep -rac '^\s*теорема ' flang --include='*.flang'`,
 сумма по `awk`).