# Часть XXV. Proof graph и объяснения ## 179. Proof graph Proof graph является DAG. Узлы: ```text assertion rule_application function_evaluation priority_decision defeat source_resolution interpretation_selection norm_creation norm_status_transition query_evaluation external_snapshot_read judgment candidate_closure constraint_check evidence_projection support_admission cone_completion ``` `evidence_projection` и `support_admission` — узлы acceptance-фазы §78.2.7 (DECISION-0126). Первый есть ЛИСТ: спроецированный факт сырого evidence/support/verification, у которого нет ни origin §73, ни временных осей §72, и потому он не `assertion`. Второй свидетельствует РЕШЕНИЕ о принятии опоры: его вывод — принятый литерал нужной полярности, посылки — применения правил политики, атрибуты называют политику, профиль, ребро §75, связь и документ. Нормативный факт, принятый политикой, несёт `support_admission` среди оснований и узла `assertion` НЕ имеет: подделать его, не предъявив опору и правило, нельзя структурно. `constraint_check` — узел ground constraint application §93.3 (errata E-0086): свидетельствует вердикт §93.1 под подстановкой и называет опоры, прочитанные antecedent и requirement. `cone_completion` — узел завершения конуса вопроса §181.3 (DECISION-0368). Он бывает ТОЛЬКО в документе `law.core.focused-evaluation/0.1`: утверждает, что подпрограмма конуса доведена до фикспойнта, и проверяется повторным выводом конуса. В полном документе §208 такого узла нет. `candidate_closure` — узел сертификата §181.1: он свидетельствует не вывод, а ПОЛНОТУ перебора кандидатов конфликтной группы, и потому назван здесь наравне с прочими видами (errata E-0030). Перечень **закрыт**: вида узла, которого в нём нет, в графе быть не может. Закрытость записана прямым предложением, а не оставлена выводимой из перечня, — на ней держатся квалификации отказов проверяющего (узел, не находящий себе вида, есть дефект эмиттера, а не повод завести вид молча). Граф **замкнут по посылкам**: каждый идентификатор в `premise_nodes` (`premises` в `evaluation.schema.json`) обязан разрешаться в узел ЭТОГО ЖЕ графа. Требование не следует из «DAG» и потому записано отдельно: граф с висячим ребром остаётся ациклическим на своих узлах, а проверяющий не может отличить пропущенный узел от подделанной ссылки — обе выглядят одинаково (errata E-0019). Замкнутость касается ТОЛЬКО посылок — рёбер вывода. Поля `rule`, `interpretation`, `sourceAnchors` и `evidence` указывают за пределы графа (в CLIR, в source model, в материалы дела) и разрешаются своими средствами; требовать их присутствия в графе значило бы вкладывать в доказательство саму программу. ## 180. Rule application proof ```text rule_application { id; rule; substitution; body_result; premise_nodes; applicability; source_anchors; interpretation; conclusion; } ``` Соответствие имён в `evaluation.schema.json`: `premise_nodes` → `premises`, `applicability` → `applicabilityStatus` (ср. §179). `body_result` отдельным полем не сериализуется: тело применения восстановимо из `rule` (правило в CLIR) и `substitution`, и проверяющий пересчитывает его сам (§197), а не читает утверждение движка о собственном выводе. Обязательность `rule`/`substitution` у узла этого вида выражена схемой (errata E-0022): узел без пары-свидетельства — не применение. **Идентификатор узла (errata E-0125; заменяет E-0097).** `id` узла `rule_application` есть `urn:proof:apply:<хвост правила>:`. `` — полный, неусечённый SHA-256 канонических байт §208 кортежа из полного StableId правила, подстановки, канонического множества `premises` и `conclusion`. `<хвост правила>` остаётся только читаемой подсказкой и берётся после `#`; тождество задаёт полный хэш над полным именем правила, поэтому неоднозначные хвосты E-0097 больше не требуют отдельной схемы. Точный повтор дедуплицируется. Каноническое обоснование выбирается независимо от физической стратегии вывода: 1. узел `assertion` имеет логический ранг 0; 2. grounded-применение имеет минимальный синхронный ранг, на котором выполнены все его посылки (errata E-0241). Ранг считается по итоговому графу, а не по журналу исполнения: ранг атома равен наименьшему рангу среди узлов с этим заключением, а ранг применения равен 1 + наибольшему рангу атомов, которые служат его посылками. Момент, когда физический план впервые обнаружил применение, и опоры, существовавшие в этот момент, на ранг не влияют. Прочие узлы с посылками имеют ранг 1 + наибольший ранг своих посылок; 3. если допустимы несколько наборов опор, выбирается один witness, минимальный по паре (логический ранг, канонический кортеж id посылок); 4. naive, semi-naive, параллельный и иной физический план обязаны выбрать тот же witness; 5. одно grounded-применение представлено одним узлом: все комбинации опор отдельными узлами не материализуются. **Применение определения (DECISION-0151).** Если правило несёт ребро provenance `was_derived_from` с атрибутом `declaration: "definition"` (§144), узел `rule_application` несёт `attributes.definition` — объект с полями `concept` (StableId символа понятия — цель ребра), `mode`, `part` и, у расщеплённой достаточной половины, `alternative`. Поле копируется из ребра и в content-id узла не входит: тождество применения задают правило, подстановка, посылки и вывод. Объяснение §183 читает поле и называет шаг «по определению понятия», а не «по правилу»; машинное объяснение §184 отдаёт его списком `definitions` только при непустоте, как `a3Selections`. Та же content-адресация применяется вместо порядкового `:` у прочих видов proof-узлов: `norm_creation`, `norm_status_transition`, `defeat`, `source_resolution`, `candidate_closure`, `constraint_check`, `judgment` и `external_snapshot_read`. Их хэш считается над каноническим объектом узла без поля `id`; ранг равен нулю при отсутствии посылок, иначе на единицу больше максимального ранга посылок. Позиции норм §134 и отчёты конфликтов §115 узлами proof-графа не являются, но порядкового номера тоже не несут (errata E-0246, E-0247): отчёт адресуется своим содержанием (§115), позиция — подстановкой своего применения (§133). Изменение аннотации узла обязано адресовать его по `id`, а не по позиции в массиве. ## 180.1. Каноническое множество proof-узлов `proofGraph.nodes` является сериализацией множества, а не журналом исполнения. Единственный порядок — канонический топологический: каждая посылка стоит раньше зависимого узла, а среди всех готовых узлов первым идёт лексикографически меньший `id`. Сериализатор обязан отвергнуть висячую посылку, дубликат `id` и цикл, а не выпускать частичный либо произвольно упорядоченный граф. Массивы с семантикой множества (`premises`, `roots`, `sourceAnchors`, `evidence`, `conditionWitnesses`, перечни кандидатов замыкания и иные названные схемой множества id) сериализуются без дубликатов в лексикографическом порядке. Массив, чья последовательность нормативна (`priorityPath`, история переходов), этим правилом не переупорядочивается. Имя поля само по себе не превращает значение в множество: в частности, `candidates` у замыкания есть массив id, а одноимённое поле why-not conclusion есть числовой счётчик. Правило этого абзаца применяется только когда значение является массивом. ## 180.2. Proof-узлы свёртки процедур (DECISION-0156) Фаза свёртки §161.1 не является правилом и правилами не выражается: узлы `

/initial`, `

//valid`, `

//enters` десугаризация больше не эмитирует (§201.1). Поэтому обосновать её выводы узлом `rule_application` §180 нельзя — тот требует пары «правило + подстановка», а её нет; у `current_state(x, S)` проверяемого основания нет и подавно: он есть проекция КОНЦА истории, а не следствие одного шага. Вводятся два вида узлов. **`procedure_step` — один ШАГ свёртки, а не одна попытка.** Единицей узла служит носитель: шаг §161.1 атомарен и может нести несколько переходов в попарно независимых областях §162.1, поэтому узел выпускается ОДИН на пару «экземпляр, носитель» и перечисляет все попытки этого носителя — включая невалидные: попытка, не породившая эффекта, есть штатный исход §164, и объяснить её обязан тот же граф. Атрибуты: **Имена атрибутов нормативны.** Карта атрибутов proof-узла есть свободный `JsonValue` (§180), и потому имена полей не выражаются схемой ничем: две реализации, эмитирующие одни и те же сведения под разными именами, разошлись бы байтово при зелёных схемах. Таблица ниже закрывает их поимённо. | Атрибут | Значение | |---|---| | `procedure` | StableId узла `procedure` §201.1 | | `instance` | экземпляр `x` | | `carrier` | `id` события-носителя — ГОЛОВЫ цепочки версий §81.1 | | `transitions` | массив попыток шага: у каждой — `transition` (StableId перехода `T`), `outcome` (`valid` либо `invalid`) и, при `invalid`, `reason` — невыполненное условие | | `stateBefore` | состояние (или множество токенов областей §162.1) перед носителем | | `outcome` | `valid`, если валиден хотя бы один переход шага, иначе `invalid` | | `reason` | при `outcome: invalid` — невыполненное условие шага; есть ТОЛЬКО у шага из одного перехода и совпадает с `reason` его единственного элемента `transitions`. У шага из нескольких переходов атрибут ОТСУТСТВУЕТ — и отсутствует даже тогда, когда причины всех попыток совпали: причина принадлежит ПОПЫТКЕ, а не шагу, и читается по элементам `transitions` формы `{transition, outcome, reason}` | | `supersedes` | `id` исправленной версии носителя §81.1; присутствует, когда носитель есть голова непустой цепочки, и отсутствует иначе | Массив `transitions` есть МНОЖЕСТВО в смысле §180.1 и сериализуется в лексикографическом порядке StableId перехода, а не в порядке предъявления попыток делом: порядок внутри шага семантики не имеет (§161.1), и брать его из дела значило бы делать proof-граф функцией записи фактов. Тем же порядком обеспечена независимость `id` узла от неё: хэш §180 берётся над каноническим объектом, в который массив входит уже отсортированным. При `outcome: invalid` у попытки узел называет ПРИЧИНУ полем `reason`, и словарь причин закрыт ПЯТЬЮ значениями: четыре условия валидности §161.1 — `from`, `on`, `guard`, `requires` — и пятое, `join`: политика соединения §162.2 не удовлетворена. Пятое стоит отдельно, а не внутри `from`: переход соединения ведёт из состояния, в котором экземпляр И НАХОДИТСЯ, и назвать его невалидным «по `from`» значило бы соврать о состоянии. Различение это не удобство отчёта: без него «переход не состоялся» неотличимо от «переход не рассматривался», а why-not §185 обязан различать их. Заключениями узла служат опубликованные факты ВСЕХ валидных переходов шага: `valid_transition(x, T, e)`, `left_state(x, …, e)` (все публикуемые §162.1) и `entered_state(x, to(T), e)`. Посылками `procedure_step` являются: узлы попыток `attempted_transition` (`assertion` либо применение, их произведшее), `procedure_step` предыдущего события того же экземпляра — если оно есть — и узлы опор гардов и `requires`. Ребро на исправленную версию носителя §81.1 присутствует, когда носитель есть голова непустой цепочки: ответ, опирающийся на исправленное время, обязан показывать, чтó было исправлено. **`procedure_history` — итог свёртки экземпляра.** Один узел на экземпляр, и он выпускается ДАЖЕ У ЭКЗЕМПЛЯРА С ПУСТОЙ ИСТОРИЕЙ: начальное состояние §161.1 есть факт `initial_state(x, S_initial)`, и обосновать его нечем иным. Атрибуты — так же поимённо: `instance`; `initialState` — начальное состояние, заключением которого служит `initial_state(x, S)`; `carriers` — УПОРЯДОЧЕННЫЙ список идентификаторов носителей в порядке истории (массив НОРМАТИВНОЙ последовательности, §180.1 его не переупорядочивает); `states` — итоговые состояния (одно у простой процедуры, по одному на область плюс составное — при §162.1); `complete` — достигнуто ли терминальное состояние. Заключениями узла служат `initial_state(x, S_initial)` и `current_state(x, S)`: именно `procedure_history` есть обоснование обоих, и ответ о состоянии дела без этого узла считается несформированным (§179). Посылки — все `procedure_step` того же экземпляра; у экземпляра с пустой историей посылкой служит узел факта `procedure_instance(x)`. Хвост `procedure_step` берётся от НОСИТЕЛЯ, а не от перехода, и это следует из единицы узла: шаг атомарен и может нести несколько переходов в независимых областях §162.1, поэтому единственного перехода у него нет — прежняя редакция называла форму, которой у узла быть не может. Идентификаторы обоих видов строятся по §180 content-адресацией: `urn:proof:procedure-step:<хвост НОСИТЕЛЯ>:` и `urn:proof:procedure-history:<хвост экземпляра>:`, где хэш берётся над каноническими байтами §208 объекта узла без поля `id`. ## 181. Priority proof Каждое `defeat` в `law.core/0.2` несёт обязательный исход `outcome: DEFEATED` и обязательный `priorityPath`. Пустой путь допустим только для поражения строгой противоположностью либо дефитером: победа там не читает порядок §106. Поражение с причиной `priority` или `norm_conflict` имеет непустой путь. Каждый шаг `priorityPath` содержит `priorityRule`, `higher`, `lower` и `conditionWitnesses`. `priorityRule` разрешается ровно в объявленный узел `priority_rule` CLIR. Для безусловного порядка `higher`/`lower` — стороны этого объявления; транзитивный порядок сериализуется цепочкой объявленных рёбер, без сокращённого выдуманного ребра. Для условного порядка стороны — StableId фактически сравнивавшихся grounded applications, а `conditionWitnesses` — proof-узлы опор, на которых условие получило `TRUE_ONLY`. Путь выбирается детерминированно: кратчайший, затем лексикографически первый по StableId объявления. Таким образом, каждое defeat должно ссылаться на: - attacking application; - attacked application; - priority declaration/policy; - context facts, удовлетворившие policy; - source anchors priority rule. ## 181.1. Candidate closure certificate Положительный defeasible вывод требует доказать не только наличие supporting candidate, но и отсутствие пропущенного более сильного opponent. Поэтому каждый resolved conflict group имеет closure certificate: ```text program_semantic_hash evaluation_input_semantic_hash stratum conflict_key all_applicable_candidate_ids | merkle_commitment priority_graph_hash ``` Proof checker либо получает полный список candidates, либо проверяет Merkle commitment относительно EPlan/candidate index. Без closure certificate proof считается explanatory, но не cryptographically/audit complete. Why-not, weak permission и violation-by-absence также требуют соответствующего domain/closure certificate. ## 181.2. Total outcome при блокирующей диагностике Issue с severity `error` или `fatal` является блокирующим. Ни один result того же evaluation-документа не может при этом иметь `evaluationStatus: COMPUTED`: если специальный статус для кода объявлен §175, используется он, иначе `NON_EXECUTABLE`. Это правило применяется ко всем видам запроса, а не к веткам, которые случайно не забыли проверить конкретный код. **Ошибка терма правила блокирует только зависимый результат (errata E-0192).** Issue, выпущенная ошибкой вычисления терма §58 при применении правила `R` (§175, errata E-0105; носитель — `relatedNodes: [R]`), отвечает за выводы, которые это правило могло бы дать, и за всё, что от них зависит, — и только за них. Результат ЗАВИСИТ от `R`, если предикат его вопроса лежит в замыкании от головы `R` по рёбрам предикатного графа §110 — тем же, что у стратификации и у зависимости от неразрешённого прочтения §156 (errata E-0140): ребро даёт каждый конъюнкт тела, включая негатив, `not_known`, статус-тесты и кванторы, а дефитер §95.3 производит предикат поражаемого вывода. Вопрос `truth`, `why_not` — по предикату литерала; `collect` и `formula` — по любому предикату внутри терма вопроса; у `positions` и прочих видов вопроса зависимость не разбирается, и они считаются зависимыми. Разбор ведётся по КАЖДОМУ упавшему правилу отдельно (errata E-0242): уровень issue называет её собственный носитель, и зависимость результата от одного правила не делает блокирующей issue другого. В документе НЕЗАВИСИМОГО результата такая issue сохраняет код, сообщение и адрес правила, но получает `severity: warning` и блокирующей не является: «право не посчитано» относится к неустойке, а не к дню срока, который её не читает. В документе зависимого результата ничего не меняется: `error`, статус по §175 либо `NON_EXECUTABLE`. Граница проведена по ПРОГРАММЕ, а не по делу: зависимость есть свойство предикатного графа, и пустое на данном деле тело её не снимает — ошибка в безопасную сторону. `MISSING_PARAMETER_VALUE` (errata E-0171) остаётся `warning` всегда. Правило действует там же, где сам total outcome, — с семантики 0.2: документ 0.1 блокирующих issue к результатам не применяет, и уровень его issue не меняется. **Конфликт ключа отношения блокирует только зависимый результат (errata E-0210).** Issue `KEY_CONFLICT` §45.1/§196 отвечает за то, что читается из отношения `R`, назвавшего её (`details.predicate`), — и только за это. Область та же, что у ошибки терма выше, и считается тем же замыканием по рёбрам предикатного графа §110: результат ЗАВИСИТ от `R`, если предикат его вопроса лежит в замыкании вперёд от `R`, где ребро даёт каждый конъюнкт тела, включая негатив, `not_known`, статус-тесты и кванторы. Отличие одно — начало замыкания: у ошибки терма это голова упавшего правила, у конфликта ключа — само отношение, поэтому вопрос о `R` зависим всегда. Разбор ведётся по КАЖДОМУ конфликтному отношению отдельно: уровень issue называет её собственный носитель, и зависимость от одной таблицы не делает блокирующей issue другой. В документе НЕЗАВИСИМОГО результата такая issue сохраняет код, сообщение и адрес утверждений, но получает `severity: warning` и блокирующей не является: «таблица коэффициентов противоречива» относится к делу, где эта таблица открыта, а не к делу, которое её не читает. В документе зависимого результата ничего не меняется: `error` и `NON_EXECUTABLE`; ничего не выбирается и не удаляется по-прежнему — §45.1 правится не здесь. Граница проведена по ПРОГРАММЕ, а не по делу, и действует с семантики 0.2 — оба условия те же, что у ошибки терма. Пакет, чьи СОБСТВЕННЫЕ ground-утверждения конфликтуют по объявленному ключу, до всякого вычисления отвергается статически (§196, `LDC-E1368`); это правило о конфликте, принесённом ДЕЛОМ. **Нарушенное ограничение блокирует только зависимый результат (errata E-0236).** Issue `CONSTRAINT_VIOLATED` и `CONSTRAINT_CONFLICTED` §93.3 уровня `error` (носитель — сам constraint `C`, `relatedNodes: [C]`) отвечает за то состояние, которое ограничение связывает, — и только за него. Результат ЗАВИСИТ от `C`, если предикат его вопроса лежит в замыкании вперёд по тем же рёбрам предикатного графа §110 от множества предикатов, которые читают клаузы `scope`, `when` (antecedent) и `require` (requirement) этого ограничения: constraint не выводит и не поражает, он спрашивает готовое состояние, и отвечает за то, что в этот вопрос входит (аналог конфликта ключа выше — отношение `R` отвечает за своих читателей). Ребро даёт каждый конъюнкт тела, включая негатив, `not_known`, статус-тесты и кванторы; начало замыкания — предикаты самого ограничения, поэтому вопрос о любом из них зависим всегда. Разбор ведётся по КАЖДОМУ ограничению отдельно: носитель назван `relatedNodes`, и зависимость от одного ограничения не делает блокирующей issue другого. Вопрос `truth`, `why_not` — по предикату литерала; `collect` и `formula` — по любому предикату внутри терма вопроса; у `positions` и прочих видов зависимость не разбирается, и они считаются зависимыми. В документе НЕЗАВИСИМОГО результата такая issue сохраняет код, сообщение, `relatedNodes` и `details`, но получает `severity: warning` и блокирующей не является. В документе зависимого результата ничего не меняется: `error` и `NON_EXECUTABLE`. Сам результат `CONSTRAINT` в `results[]` этой границей не затрагивается: у него собственный вердикт §93.3. Объявленная у ограничения `severity: warning` блокирующей не была и не становится; `critical` (записывается как `error` с `details.severity`) ведёт себя как `error`. Граница проведена по ПРОГРАММЕ, а не по делу, и действует с семантики 0.2 — оба условия те же, что у ошибки терма и у конфликта ключа. **Ошибка типа, отказ канала суждения и цикл приоритетов блокируют только зависимый результат (errata E-0243, E-0244, E-0245).** Issue уровня `error` с кодами `TYPE_ERROR`, `JUDGMENT_AUTHORITY_MISMATCH`, `JUDGMENT_PAYLOAD_MISMATCH` и `PRIORITY_CONFLICT` отвечает за предикат своего носителя — и только за его читателей: - `TYPE_ERROR` (E-0243) — предикат `details.predicate`. У утверждения §189 это его предикат, у вывода E-0077 — голова правила, чей вывод не принят; - `JUDGMENT_AUTHORITY_MISMATCH` и `JUDGMENT_PAYLOAD_MISMATCH` (E-0244) — предикат утверждения, названного `relatedNodes`, чей ответ органа §47.3.1 не принят; - `PRIORITY_CONFLICT` (E-0245) — головы правил конфликтной группы, названных `relatedNodes`. У рантаймового цикла §121 там названы узлы приоритетов, и берутся головы правил, на которые они ссылаются (`higher`, `lower`) — надмножество группы, ошибка в безопасную сторону. Результат ЗАВИСИТ от issue, если предикат его вопроса лежит в замыкании вперёд от этих предикатов по тем же рёбрам графа §110, что у E-0192, E-0210 и E-0236. Носитель, которого разбор не находит, делает результат зависимым. Разбор ведётся по КАЖДОЙ issue отдельно. В документе НЕЗАВИСИМОГО результата issue сохраняет код, сообщение, `relatedNodes` и `details`, но получает `severity: warning` и блокирующей не является: утверждение постороннего субъекта с целым в неверной форме не гасит ответ о субъекте, которого вопрос касается. В документе зависимого результата ничего не меняется. Граница проведена по ПРОГРАММЕ, а не по делу, и действует с семантики 0.2. Отказы подготовки, не называющие носителя (`ASSERTION_ID_COLLISION`, `CONFLICTED_INPUTS`, выбор календаря и другие уровня `fatal`), остаются общими для документа. Total outcome читает issue уже ПРЕДЪЯВЛЕННЫЕ, а не всякую, прозвучавшую по ходу вывода (errata E-0198). Ошибка терма, выпущенная проверкой монотонного агрегатного гарда §111, предъявляется по состоянию неподвижной точки страты этого правила: ошибка промежуточного раунда, не повторившаяся на последнем, в документ не попадает и потому ничего не гасит, а ошибка на закрытой страте блокирует зависимый результат по общему правилу выше. Порядок здесь содержательный: до errata ложная `EMPTY_AGGREGATE` первого раунда превращала в 0.2 верный `TRUE_ONLY` в `NON_EXECUTABLE`. ## 181.3. Полнота относительно вопроса (`focused_truth`, DECISION-0368) **Норма — проекция полного ответа.** Документ вопроса `focused_truth(q)` задаётся функцией `ProjectFocused(D)`, где `D` — полный документ §208 вопроса `truth` о том же литерале. Вопрос `q′` получается из `q` заменой вида на `truth`, с тем же `queryId`, над тем же предъявленным миром, делом и опциями. Реализация обязана выдавать ровно байты `ProjectFocused(D)`. Способ вычисления — полный вывод или вывод подпрограммы конуса — байтов не меняет и в семантические хэши не входит (§280.4). **Конус вопроса** `C(q)` — наименьшее множество предикатов программы, для которого выполнены три условия: 1. `pred(q) ∈ C(q)`. 2. Если потребитель ребра графа §110 лежит в `C(q)`, его производитель тоже лежит в `C(q)`. Рёбра — те же, что у замыканий §181.2: конъюнкты тела любой полярности и статуса, кванторы и генераторы агрегатов, status-тесты условных термов, вершины замыканий §70 с их доменами, головы дефитеров §95.3. 3. Если ограничение §93.3 читает клаузами `scope`, `when` или `require` хотя бы один предикат `C(q)`, все читаемые им предикаты входят в `C(q)`, а само ограничение входит в конус. Ограничение, не читающее ни одного предиката, входит в конус всегда (§181.2, E-0236). Конус считается над узлами вида программы после изоляции прочтений §152–§156 и проекции редакций §92.3. `coneHash` — хэш §208 массива предикатов `C(q)` в каноническом порядке строк. **Вне профиля первого среза.** Вопрос отвергается до вычисления issue `FOCUS_OUT_OF_PROFILE` (fatal), без результата и без proof, если `C(q)` пересекает: - предикаты, достижимые от голов эффектов полномочий §127 (`effect_reachable_predicates`, E-0134); - предикаты, публикуемые свёрткой процедур §161.1. `details.reason` называет причину, `details.predicates` — пересечение в каноническом порядке. **Проекция `ProjectFocused(D)`.** 1. **Отказ.** Если в `D` нет результата вопроса, документ повторяет `issues` полного документа, `results`, `conflicts` и proof пусты. 2. **Результаты.** Первым идёт результат вопроса из `D` без изменений полей, кроме адресов отчётов конфликтов (п. 5). За ним — результаты ограничений конуса в порядке `D`. 3. **Узлы proof.** Из канонического графа `D` берутся узлы, у которых: - заключение — литерал предиката конуса (`rule_application`, `defeat`, `candidate_closure`, `evidence_projection`, `support_admission`); - либо это `constraint_check` ограничения конуса; - либо это `interpretation_selection` или `source_resolution`. Затем множество замыкается по всем ссылкам на узлы графа — `premises`, `conditionWitnesses` и id узлов в атрибутах. Узел `assertion` затравкой не служит: он появляется в графе, когда утверждение стало чьей-то посылкой, и в `D` его могло создать правило вне конуса. В срез он входит только замыканием. Узлы переносятся без изменений, id — те же, что в `D`. 4. **Корень вопроса.** Узел корня `D` переносится с видом `query_evaluation` и атрибутом `queryKind: "focused_truth"`. Его посылки дополняются узлом завершения. Узел завершения `cone_completion`: - посылки — все `candidate_closure` среза; - заключение — `{"cone": coneHash}`; - атрибуты — `programSemanticHash` и `evaluationInputSemanticHash` (значения `programHash` и `caseHash` манифеста `D`) и `coneHash`; - id — `urn:proof:cone-completion:` над объектом без `id`. Узел завершения утверждает, что подпрограмма конуса доведена до фикспойнта по всем стратам. Проверяется повторным выводом конуса. Порядок узлов — канонический топологический §180.1 над срезом. 5. **Отчёты конфликтов.** Отчёт входит, если его атом — литерал предиката конуса. id отчёта уже контентный (§115, errata E-0246) и в срезе не меняется; ссылки результата остаются прежними. 6. **Issues.** Входит каждая issue уровня `error` и `fatal` документа `D` (§181.2 уже понизил независимые от вопроса). Issue уровня `warning` и `info` входит, если её носитель лежит в конусе: - `relatedNodes` называет правило с головой из конуса, утверждение предиката конуса или ограничение конуса; - либо `details.predicate` — предикат конуса. Порядок — порядок `D`. 7. **Прочее.** `evidenceAcceptance` §78.2.7 переносится без изменений. `positions` в документ не входят. **Форма документа** (`law.core.focused-evaluation/0.1`): - `schemaVersion`, `evaluationKind: "focused_truth"`; - `manifest` — манифест `D` без изменений; - `focusManifest` — `contract: "law.focus/0.1"`, `queryId`, `profile: "i-relational-defeasible"`, `completeness: "query"`, `leanCompleteness: "not-certified"`, `cone: {predicates, coneHash}`; - `results`, `conflicts`, `proofGraph` (`nodes`, `roots` и `focusedProofHash`), `issues`, при наличии `evidenceAcceptance`; - `answerHash`, `focusedResultHash`. Хэши считаются по §208 над объектом `{"domain": ":<имя>", "value": <содержимое>}`: - `focusedProofHash` — над `{nodes, roots}`; - `answerHash` — над `{queryId, target, truthStatus, evaluationStatus, missingInputs, judgmentRequests}` результата вопроса (`null` при отказе); - `focusedResultHash` — над документом без `focusedResultHash` и `executionReceipt`. Полные `proofHash` и `resultHash` §208 документ не несёт. **Равенство с полным ответом.** `truthStatus`, `evaluationStatus`, `missingInputs`, запросы судье и отказ совпадают с `D` по построению. Для вывода подпрограммы конуса тем же порядком правил и проходов подграф п. 3 совпадает с узлами, которые даёт этот вывод (DECISION-0368 §3.6). Реализация вправе опираться на это только там, где статический квалификатор DECISION-0368 §3.8 исключил источники глобальных отказов вне конуса. ## 182. Source resolution proof Dynamic reference proof содержит: - исходный Work ID; - resolver policy; - legal time; - language; - найденный exact edition; - rejected candidates; - content hash. ## 183. Human-readable explanation Human renderer строится только из proof graph и source labels, а не из скрытого reasoning. Пример: ```text Требование к безопасному расстоянию применимо, поскольку событие относится к взрывным работам и редакция пункта 125(3) действовала на 25 августа 2026 года. Для массы заряда 500 kg формула даёт 320 m. Зафиксировано 280 m. Обязанность поддерживать расстояние не менее 320 m нарушена на 40 m. ``` ## 184. Machine explanation ```json { "conclusion": "violated:position-17", "because": [ "rule-application:bvr-distance-17", "calculation:required-distance-500kg", "assertion:measured-distance-280m" ], "sourceAnchors": ["fragment:bvr-125-3-ru"], "evidence": ["evidence:measurement-17"] } ``` ## 185. Why-not `why_not(P)` строит blocker graph: - rule body false/refuted; - missing fact; - conflicting premise; - defeated rule; - source not in force; - wrong interpretation; - missing judgment; - unresolved reference. Why-not не должен утверждать, что отсутствующее условие ложно. Путь запроса судьи §47.3 читает тот же blocker graph, и виды блокеров здесь не складываются: правило, у которого один конъюнкт «rule body false/refuted», ДРУГОГО своего конъюнкта как «missing judgment» не выставляет — оно мертво, и ответ судьи исход не изменит (errata E-0101). Отчёт `why_not` при этом называет оба конъюнкта как есть: `NOT_SATISFIED` у опровергнутого, `UNDETERMINED` у судейского. Ошибка терма правила-кандидата — блокер своего рода (errata E-0105): `why_not` при `NEITHER` кладёт рядом с `blockers` список `termErrors` — по записи `{rule, code, message}` на пару (правило, код) из issues вычисления, найденную обходом §175 по совместимым головам, — и несёт тот же статус §175 с `missing_inputs`. Поле пишется только непустым. Правило, чья голова содержит вычисляемый аргумент (`call` §86, арифметика §58, `let`), попадает в `blockers` по СОВМЕСТИМОСТИ головы с целью, а не по равенству (errata E-0164): вычислять в объяснении нельзя, поэтому равенство такого аргумента с аргументом цели не проверяется, связанные аргументы подставляются в тело как обычно, а блокер несёт список `headArguments` — по записи `{position, term, status: "UNEVALUATED", detail}` на каждый вычисляемый аргумент головы, в порядке позиций. Поле пишется только непустым; прочие поля блокера те же. Такой блокер отвечает на «почему правило не вывело ничего при этих связанных аргументах», а не «почему не именно это значение»: при выполненном теле (`trigger: SATISFIED`) правило могло вывести ДРУГОЕ значение того же предиката, и отчёт этого не различает — сравнение значений было бы вычислением. Ошибку терма такого правила по-прежнему называет `termErrors`. До errata правило с вычисляемой головой в `blockers` не попадало вовсе, и на вопрос «почему выплата не 850 000» отчёт разбирал только альтернативу с литеральной головой — не ту, что спрашивали. Так же не складываются «defeated rule» и «missing judgment» (errata E-0103): поражаемое правило, чей вывод поразил бы уже сработавший и не побеждённый приоритетом §106 дефитер §107.3, судью не называет; отчёт `why_not` несрабатывание поражаемого правила по-прежнему объясняет механикой §107–§108, не конъюнктами. Конъюнкт с экзистенциальным аргументом `_` §98 (errata E-0165) отчёт не связывает целью и не перечисляет за него значений: при найденном свидетеле существования — `SATISFIED` с `detail` «есть значение (§98, E-0165)», без единого подходящего атома — `UNDETERMINED` с «нет ни одного значения (§98, E-0165)»; `literal` отчёта — образец с подчёркиванием, связанные аргументы подставлены. Обход транзитивных блокеров §175 и перечисление кандидатов судьи через такой конъюнкт не идут: цели с `_` не бывает. Живых ветвей бывает несколько, и у каждой свой судья (errata E-0111). Путь запроса §47.3 перечисляет КАЖДОГО судью, чей ответ способен разблокировать вывод: обход блокеров ключует посещённое парой (предикат, полярность), отрицательный литерал спускается в правила с отрицательной головой того же предиката, и ветвь, дошедшая до атома первой, не закрывает его противоположность для второй. Порядок элементов `results[].judgmentRequests` — по каноническим байтам §208 объекта `request` (отношение, полярность, аргументы); нумерация proof-узлов `judgment` следует этому порядку. До errata реализации ключевали посещение без полярности, и на поражаемой развилке `g ⇐ p` / `g ⇐ q ⇐ not p` одна называла судью ветви `p`, другая — судью ветви `not p`: ответ зависел от порядка обхода, а не от права. Путь запроса судьи связывает переменные правила, не связанные целью, свидетелями store (errata E-0189, §47.3): ground-атом, совпавший с положительным литеральным конъюнктом того же правила, продолжает подстановку, и обход идёт в ground-подцель, которой без него не было бы. Отчёт `why_not` этим не тронут: конъюнкт с переменной, не связанной целью, в нём по-прежнему `UNDETERMINED` с «переменные не связаны целью», и подстановок за него отчёт не перечисляет. ## 185.1. Why-not над предикатами свёртки (DECISION-0156) Предикаты §164.1 правилами не производятся: узлы `

/initial`, `

//valid`, `

//enters` десугаризация больше не эмитирует (§201.1), а исход попытки лежит proof-узлом `procedure_step` §180.2. Обход §185 по кандидатам-правилам на такой цели молчал бы — и это молчание неотличимо от «блокеров нет». Поэтому у целей `valid_transition(x, T, e)`, `entered_state(x, S, e)` и `current_state(x, S)` кандидатом служит ПЕРЕХОД, а не правило, и blocker graph строится ЧТЕНИЕМ уже вычисленного: ничего заново здесь не считается, свёртка §161.1 прошла до запроса. Кандидаты выбираются по виду цели: у `valid_transition` — переход, названный вторым аргументом; у `entered_state` и `current_state` — ВСЕ переходы, чей `to` есть названное состояние (без такого чтения вопрос «почему дело не в `S`» не имел бы ответа вовсе). Носитель берётся третьим аргументом цели, а у `current_state`, проекции конца истории §164.2, — последним носителем `procedure_history` того же экземпляра. Носитель ищется и по исправленным версиям §81.1: спрашивающий называет ту версию, что у него на руках, а шаг привязан к голове цепочки. Запись блокера — та же, что у правила (`rule`, `applicability`, `trigger`, `conjuncts`), и `rule` несёт StableId ПЕРЕХОДА: наблюдения §267 `blocked_by()` и `blockers(n)` работают без нового словаря, а причина шага §180.2 читается вторым аргументом `blocked_by(, "<причина>")` — из `detail` блокера, дословно (§267.4). Три исхода: - **попытки нет.** `attempted_transition(x, T, e)` в истории отсутствует — переход не рассматривался, а не «условие не выполнено». Блокер называет недостающей посылкой саму попытку, тем же конъюнктом §65, каким называется недостающая посылка правила; `trigger` — `UNDETERMINED` (§185 запрещает утверждать, что отсутствующее ложно). У `current_state` экземпляра с пустой историей носителя нет вовсе, и конъюнкт называет это прямо. - **попытка есть и шаг валиден.** `trigger` — `SATISFIED`, и блокер говорит, что причина не в условиях §161.1 (симметрично «тело выполнено — причина не в конъюнктах»). - **попытка есть и шаг невалиден.** Недостающие посылки следуют `reason` §180.2: `from` — литерал `state_before(x, from(T), e)` (§164.2); `on` — сверка типа носителя с `on E` §160.1, поверхности литерала не имеющая; `guard` и `requires` — ТЕ ЖЕ конъюнкты, что у правила, полученные разбором формулы условия при подстановке экземпляра; `join` — политика соединения §162.2 с токенами областей из `stateBefore` шага. Граница названа, а не обойдена: конъюнкты гарда размечаются по ИТОГОВОМУ store, тогда как свёртка читала префикс §161.2. Барьер §161.2 иного и не допускает у предикатов ниже свёртки, и там они совпадают; гард, читающий свёртку ДРУГОГО экземпляра §163.1, может разойтись с итогом — тогда сводка блокера остаётся `UNDETERMINED` и выполненной посылку не объявляет. ## 186. Counterfactual Counterfactual query требует: ```text target mutable inputs immutable inputs cost function legal constraints interpretation/context ``` Без cost function понятие «минимальное изменение» неопределённо. В Core 0.1 counterfactual понижается в `CounterfactualDecl`: `target`, `mutable`, `immutable`, `costModel`, `constraints` и metadata. Набор миров не выводится неограниченным решателем: вход `law.core.counterfactual-input/0.1` предъявляет конечный, content-addressed набор candidate patches, закреплённый `programHash`, `caseHash`, StableId декларации и StableId cost model. Стоимость кандидата — канонический неотрицательный Decimal. Patch меняет только case и содержит операции `setConst`, `addAssertion`, `removeAssertion` по StableId либо `setContext`. Цель каждой операции обязана входить в `mutable`; совпадение с `immutable` запрещает изменение независимо от `mutable`. Law program, выбор interpretation, evidence snapshot, calendar и external snapshots неизменяемы. После `setContext` effective context проходит полную обычную materialization/validation, а не локальную проверку поля. Solver сначала вычисляет исходное дело. `TRUE_ONLY` target даёт `ALREADY_SATISFIED`, пустой patch и стоимость `0`. Иначе кандидаты сортируются по точной Decimal-стоимости, затем StableId. Кандидат успешен только если target и все constraints имеют статус `TRUE_ONLY`: `BOTH` и `NEITHER` успехом не являются. После первого успеха solver обязан проверить весь тот же cost tier и вернуть все равноминимальные решения в canonical order; кандидаты более дорогого tier не вычисляются. Полный перебор без успеха даёт `NO_SOLUTION`. Любой fatal или незавершённый кандидат до доказанного cutoff, включая отсутствующий pinned resource, даёт `COUNTERFACTUAL_SEARCH_INCOMPLETE`; частичный минимум не публикуется. Ошибки формы и binding входа используют семейство `COUNTERFACTUAL_INPUT_INVALID`, `COUNTERFACTUAL_*_HASH_MISMATCH`, `COUNTERFACTUAL_FORBIDDEN_MUTATION` и `COUNTERFACTUAL_COST_MODEL_MISMATCH`. Результат `law.core.counterfactual-result/0.1` закрепляет входные hashes, профиль `law.solver.finite-enumeration/0.1`, все решения и replay certificate: hash канонически упорядоченного candidate set, проверенные StableId/стоимости, target/constraint statuses, evaluation hashes и cutoff. Certificate verifier повторяет конечный поиск и сравнивает весь canonical result; проверка отдельных полей сертификатом не считается. Пример: ```law counterfactual MakeCompliant { target compliant(Project17, BVR_DISTANCE); mutable measured_safety_distance; immutable charge_mass, source_rules, evidence_history; cost absolute_quantity_change; } ``` ## 187. Proof hash Canonical proof graph сериализуется детерминированно и получает content hash. Одинаковый manifest и implementation-conformant semantics должны давать одинаковый conclusion graph; renderer text может различаться без изменения proof hash. ---