the-homeless-god · Oct 6, 2026 · Oct 5, 2026 · Oct 5, 2026 · Oct 5, 2026 · Oct 5, 2026
diff --git a/.flangrc b/.flangrc
@@ -68,6 +68,10 @@ script.ring-rules:probe = bootstrap/flang io flang/proof/probes/ring-laws/run.fs
 script.translation:check = bootstrap/flang io flang/translation/run.fscript --plan Проверка
 script.proved-share:check = bootstrap/flang io flang/proof/share-measure.fscript --max-steps 4000000000 --timeout 900000 -- --set corpus
 script.proved-share:forgery = bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000
+script.lean-rules:check = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Check
+script.lean-rules:census = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Census
+script.lean-rules:numbers = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Numbers
+script.lean-rules:forgery = bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Forgery
 script.kernel-verdict:check = bootstrap/flang io flang/proof/kernel-verdict.fscript --max-steps 4000000000 --timeout 900000
 script.kernel-verdict:forgery = bootstrap/flang io flang/proof/kernel-verdict-forgery.fscript --max-steps 4000000000 --timeout 900000
 script.proof-records:freshness = bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -164,8 +164,8 @@ permissions:
 
 jobs:
   # ДИСЦИПЛИНА СЕМЕНИ идёт ПЕРВОЙ. Она читает `.flang` дерева и `bootstrap/*.c`
-  # планом на flang — 1152 файлов; разбор в задаче 5821.
-  # СНЯТО 2026-10-05 файлов *.flang = 1152 (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него
+  # планом на flang — 1153 файлов; разбор в задаче 5821.
+  # СНЯТО 2026-10-06 файлов *.flang = 1153 (задача 4791: программа-проба захвата под связывателем; до них 1152, снято 2026-10-05) (задача 5243: тринадцать программ набора проб точного дробного; до них 1139, снято 2026-10-04) (партия печати 2: десять программ проб точного целого и одна проба кольцевых законов; до них 1128, снято 2026-10-04) (модуль русской морфологии; до него
   # 1127, снято 2026-10-04) (задача 1116: три программы пробы
   # поверхностей вердикта о прогонах и задача 1113: семь программ пробы
   # порядка списков ввоза; до них 1117, снято 2026-10-04) (две честные пары
@@ -1168,6 +1168,34 @@ jobs:
         env:
           FLANG_TMP: ${{ runner.temp }}
 
+  # КАЖДЫЙ ПРИЁМ СВЕРЩИКА — С ТЕОРЕМОЙ ИЛИ СО СТРОКОЙ ДОЛГА (ADR-0064). Сторож
+  # читает `шаг_вывода` в checker.c, закрытый список приёмки Acceptance.lean,
+  # имена теорем Rules.lean и Term.lean и таблицу долга
+  # flang/proof/tables/lean-acceptance-debt.tsv; Lean ему не нужен, поэтому он
+  # идёт на каждый пуш, а не ночью со сверкой. Замер 5 октября 2026: приёмов 83,
+  # в приёмке 78, в долге 5. Заведён потому, что Н6 и О9 (задача 1435, 26 сентября)
+  # девять дней не имели теоремы, а проза считала «76 из 81» от руки. Сначала
+  # подлог: три порчи копий, каждая обязана покраснеть, иначе сторож слеп.
+  lean-rules-guard:
+    name: lean-rules-guard
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+      - run: make -C bootstrap -j"$(nproc)"
+      # Зовётся ФАЙЛОМ и в условии: прибор проб порчи
+      # (scripts/guards/guards-without-forgery-probe.fscript) признаёт пробу
+      # только по вызову в `if` с `exit 1` в том же теле и относит её к сторожу
+      # по файлу. План «Forgery» кончается кодом 0, когда все три порчи
+      # покраснели, и кодом 1, когда хоть одна прошла, — отсюда `if !`.
+      - name: Forgery goes red
+        run: |
+          if ! bootstrap/flang io flang/proof/lean/rules-guard.fscript --plan Forgery; then
+            echo "сторож приёмов промолчал на подлоге — проверять им нечего" >&2
+            exit 1
+          fi
+      - name: Every checker move has a theorem or a debt row
+        run: bootstrap/flang run-script lean-rules:check
+
   # ВТОРАЯ ПОЛОВИНА — ЖИВОЙ ПРОГОН — на метке, и без ключа: там зовутся ОБЕ.
   # 19 мин 37 с со сборкой против границы в пять минут; на пуш она не идёт, и
   # это названо ценой, а не удобством.

diff --git a/.github/workflows/lean-crosscheck.yml b/.github/workflows/lean-crosscheck.yml
@@ -65,6 +65,16 @@ jobs:
       - name: Build flang
         run: make -C bootstrap -j4
 
+      # Каждый приём `шаг_вывода` сверщика либо в приёмке Lean, либо строкой
+      # долга с номером задачи (ADR-0064): иначе теоремы состоятельности у него
+      # нет, а сверка ниже молча считает его «вне приёмки». Н6 и О9 прожили так
+      # девять дней (26 сентября — 5 октября 2026), пока число 81 переписывалось
+      # в прозе от руки. Lean этому шагу не нужен; подлог — три порчи копий.
+      - name: Every checker move has a theorem or a debt row
+        run: |
+          bootstrap/flang run-script lean-rules:forgery
+          bootstrap/flang run-script lean-rules:check
+
       # ПОЧЕМУ ЗДЕСЬ FLANG_TMP. План просит временный каталог по образцу
       # «FLANG_TMP, а если переменной нет — /srv/tmp». `/srv/tmp` есть на машине
       # разработки и нет у работника, поэтому на работнике каталог не заводился

diff --git a/docs/adr/0036-an-exact-integer-is-a-new-kind-of-value-not-a-new-name.md b/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`,
-  10497 строк. <!-- СНЯТО 2026-10-02 строк flang/proof/checker/checker.c = 10497 (задача 4416: приём «цель постусловием» и подстановка связанных имён утверждения; до неё 10421, снято 2026-10-02) (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
+  10505 строк. <!-- СНЯТО 2026-10-06 строк flang/proof/checker/checker.c = 10505 (задача 4791: разбор случаев отказывает условию под связывателем; до них 10497, снято 2026-10-02) (задача 4416: приём «цель постусловием» и подстановка связанных имён утверждения; до неё 10421, снято 2026-10-02) (задача 2748: семь правок сверщика для пользовательских программ; до неё 10015, снято 2026-09-29) (задача 4416: сверщик читает заголовок `следует`; до неё 9904, снято 2026-09-26) (задача 1400: приёмы правил Н6 и О9 в блоке «вывод»; до них 9869, снято 2026-09-20) -->
   Она переигрывает записи и о новом виде значения не знает ничего.
 
 **И встречное число, которое меняет разговор о втором варианте.** Тип `целое`