fix(checker): reject a record whose hypothesis is not the statement's

.github/workflows/ci.yml

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

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`,
-  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) -->
+  10395 строк. <!-- СНЯТО 2026-10-02 строк flang/proof/checker/checker.c = 10395 (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
   Она переигрывает записи и о новом виде значения не знает ничего.
 
 **И встречное число, которое меняет разговор о втором варианте.** Тип `целое`

docs/adr/0050-a-reasoning-is-written-as-declared-words-and-fixed-sentences.md

@@ -57,30 +57,37 @@
 
 | модус | программа | ядро, `check --proof --strict` | независимая проверяющая программа |
 |---|---|---|---|
-| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 3, «не проверено» |
-| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 3 |
-| Celarent | `celarent.flang` | доказано, код 0 | код 3 |
-| Darii | `darii.flang` | доказано, код 0 | код 3 |
-| Ferio | `ferio.flang` | доказано, код 0 | код 3 |
+| Barbara, единичная малая посылка (Сократ) | `socrates.flang` | доказано, код 0 | код 0, «проверено» |
+| Barbara | `barbara.flang` | доказано, код 0, один шаг `затем` | код 0 |
+| Celarent | `celarent.flang` | доказано, код 0 | код 0 |
+| Darii | `darii.flang` | доказано, код 0 | код 0 |
+| Ferio | `ferio.flang` | доказано, код 0 | код 0 |
 | Camestres, прямая цель `(не x.P)` | `camestres.flang` | **отказ**, код 1: ядро не выводит отрицание | записи нет |
-| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 3 |
+| Camestres, опровержением (`утверждаем нет`) | `camestres-by-refutation.flang` | доказано, код 0 | код 0 |
 | Barbara без промежуточного шага | `barbara-without-the-middle-step.flang` | **отказ**, код 1: ядро делает один модус поненс, не цепочку | записи нет |
 | подтверждение следствия | `affirming-the-consequent.flang` | отказ, код 1, `FLANG_PROOF_STEP` на строке заключения | записи нет |
 | нераспределённый средний | `undistributed-middle.flang` | отказ, код 1 | записи нет |
 | незаконное обращение | `illicit-conversion.flang` | отказ, код 1 | записи нет |
 | отрицание антецедента | `denying-the-antecedent.flang` | отказ, код 1 | записи нет |
 | экзистенциальный импорт (Barbari) | `existential-import.flang` | отказ, код 1 | записи нет |
-| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | **код 1, «не сошлось»** |
-| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | **код 1, «допущений в записи 0»** |
-| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | код 3 |
+| Darii через `есть такой … а именно` | `darii-with-the-existence-word.flang` | доказано, код 0 | код 0 |
+| посылки только в `таких что` | `socrates-with-premises-only-in-the-statement.flang` | доказано, код 0 | код 0 |
+| посылки только в `дано` теоремы | `socrates-with-premises-only-in-the-theorem.flang` | **доказано, код 0 — дыра** (§5) | **код 1**: гипотеза не является допущением утверждения |
 | без теоремы, ядро само | `socrates-without-a-theorem.flang` | доказано, код 0 | код 3 |
 | предикаты — параметры-функции | `socrates-with-predicates-as-functions.flang` | доказано, код 0 | код 3 |
 
 Итог по вопросу (1): пять названных правильных модусов ядро доказывает, пять ошибок
-отвергает кодом 1 с именем шага. Независимая проверяющая программа ни одного вывода из
-допущений сегодня не переигрывает (шаг `по предположению` вне индукции — «на слове ядра»,
-код 3) — это её объявленная граница, а не расхождение; расхождения (код 1) ровно два, и оба
-названы в таблице.
+отвергает кодом 1 с именем шага. Независимая проверяющая программа переигрывает все пять
+сама и отвечает кодом 0. Шаг `по предположению` в утверждении без функции она выводит из
+частей его `таких что` (разобранных по `и притом`), а не из строк `дано`: промежуточный шаг
+`затем Ф` и цель обязаны выводиться одним шагом — Ф есть посылка; есть посылка `если А то Ф
+иначе да` при известном А; Ф — конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель
+`есть такой м, а именно Т, что У` читается как У с Т на месте м. Каждый шаг ещё и судится
+таблицей истинности по признакам `«x».«поле»`: нашлось присвоение, при котором посылки верны,
+а шаг ложен, — код 1 с этим присвоением; шаг верен, но не одним шагом, — код 3. Записи,
+составленные для пяти ошибочных модусов, отвергаются кодом 1. Правило стоит 102 строки кода
+`checker.c` (храповик `checker-code-lines`); пробы — семья
+`flang/proof/checker/tests/families/assumption-replay/`.
 
 Полный перебор: 256 модусов четырёх фигур прогнаны текстами через переводчик
 (`flang/proof/probes/syllogism/sentences/`, план `Binary` на 256 порождённых текстах, ключ
@@ -118,13 +125,12 @@
 «Сократ».«смертен»`. То же с постусловием: функция тождества на `неотрицательное` с
 постусловием `результат больше 0` и теоремой с `дано н больше 0` — «доказано», код 0, а
 `flang run` на нуле печатает `FLANG_PROPERTY`. Ядро не сверяет гипотезы теоремы с
-ограничениями утверждения. Независимая проверяющая программа спасает лишь тем, что не даёт
-нуля (код 3). Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md).
+ограничениями утверждения. Независимая проверяющая программа отвергает такую запись кодом 1:
+гипотеза не является допущением утверждения. Задача — [5311](../tasks/5311-a-theorem-hypothesis-is-not-checked-against-the-statement.md).
 
 Следствие для этого решения: переводчик пишет посылки **в `таких что` утверждения** — тогда
 утверждение само говорит, при каких допущениях доказано заключение, — и повторяет их в `дано`,
-потому что без строк `дано` независимая проверяющая программа отвечает кодом 1 (запись не
-несёт допущений из `таких что`).
+чтобы теорема читалась сама по себе; проверяющей программе хватает `таких что`.
 
 ## 6. Словарь и образцы предложений
 
@@ -178,9 +184,9 @@
 * **Посылки отдельными `утверждение` и шаг `по свойству`** (`programs/conditional.flang`):
   честно, но файл уходит кодом 3 «доказано ПРИ УСЛОВИИ» — посылка сама «объявлено, не
   доказано». Силлогизм — это «из посылок следует», а не «посылки верны».
-* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, а
-  независимая проверяющая программа отвечает кодом 1. Заключение пишется конъюнкцией о
-  свидетеле.
+* **Цель через `есть такой … а именно`** для частного заключения: ядро доказывает, и
+  проверяющая программа переигрывает, но конъюнкция о свидетеле короче и читается прямо.
+  Заключение пишется ею.
 
 ## 8. Цена в грамматике, если делать словом языка
 
@@ -211,8 +217,6 @@
   прямой целью, без опровержения.
 * **Цепочка охран:** повторять модус поненс до неподвижной точки, чтобы `затем` не требовался
   на каждое звено. Дёшево: перебор конечен.
-* **Проверяющая программа переигрывает `по предположению` вне индукции** и читает допущения
-  из `таких что` утверждения — иначе силлогизм навсегда «на слове ядра».
 * Если рассуждение становится файлом языка: вид файла `.рассуждение` со своим разбором (§6),
   разворачивающимся в `объект` + `утверждение` + `следует` ровно так, как печатает
   `--plan Translate`; отказ разбора называет слово и предложение.

docs/course/README.md

@@ -172,7 +172,7 @@ docs/course/check.flang: проверено — разбор, типы, заве
 | ответы девяти целей | сборка и запуск девяти напечатанных программ настоящими тулчейнами этой машины: `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`, счёт строк `пример` |
 | 53 файлов и 32 526 строки библиотеки <!-- СНЯТО 2026-10-02 файлов flang/stdlib/*.flang = 53 --><!-- СНЯТО 2026-10-02 строк-в flang/stdlib/*.flang = 32526 --> | `ls flang/stdlib/*.flang`, `cat … \| wc -l` |
-| 726 заметки, 242 примеров, 413 файл доказательств <!-- СНЯТО 2026-10-02 файлов docs/zettel/*.md = 726 --><!-- СНЯТО 2026-10-02 файлов docs/examples/*.flang = 242 --><!-- СНЯТО 2026-10-02 файлов flang/proof/*.flang = 413 (задача 5502: проба пустой ведомости flang/proof/probes/strict/programs/no-obligations.flang; до неё 320, снято 2026-09-17) --> | `ls`, `find` |
+| 726 заметки, 242 примеров, 423 файл доказательств <!-- СНЯТО 2026-10-02 файлов docs/zettel/*.md = 726 --><!-- СНЯТО 2026-10-02 файлов docs/examples/*.flang = 242 --><!-- СНЯТО 2026-10-02 файлов flang/proof/*.flang = 423 (задача 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` (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) -->
+3. **Цену для проверяющей программы.** `checker.c` (10395 строк) <!-- СНЯТО 2026-10-02 строк flang/proof/checker/checker.c = 10395 (задача 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

@@ -174,6 +174,20 @@ bootstrap/flang run-script trust:ceiling
     что тело функции: литерал, `длина`, сумма, произведение на положительный
     литерал. Неотрицательным по объявлению считается только имя, связанное `для
     всех` типом-отрезком (`неотрицательное`); ограничение `таких что` дна не даёт.
+22. **Шаг `по предположению` в утверждении без функции выводится из его посылок.**
+    Когда все шаги теоремы обоснованы `по предположению`, нет ни индукции, ни
+    случаев, а каждое высказывание собрано из признаков `«x».«поле»` (`x`
+    связан `для всех`, поле объявлено `признак` в `объект` его типа), посылками
+    служат части `таких что` утверждения, разобранные по `и притом`, — строки
+    `дано` теоремы в вывод не идут. Промежуточный шаг `затем Ф по предположению`
+    и цель обязаны выводиться одним шагом из посылок и выведенного раньше: Ф
+    есть посылка; есть посылка `если А то Ф иначе да` при известном А; Ф —
+    конъюнкция таких; цель `нет` при известных Х и `не Х`. Цель `есть такой м,
+    а именно Т, что У` сличается с обещанной и выводится как У с Т на месте м.
+    Каждый шаг ещё и судится таблицей истинности по признакам: нашлось
+    присвоение, при котором посылки верны, а шаг ложен, — «НЕ СОШЛОСЬ» с этим
+    присвоением; шаг верен, но не одним шагом, — место остаётся на слове ядра.
+    Пробы — `tests/families/assumption-replay/`.
 
 Сверх того: **ни одной непрочитанной строки**. Строка записи, вид которой
 чекеру не известен, — отказ, а не «ладно». Мутационная проба (3000 порченых