# Часть XV. Defeasible semantics и conflict resolution

## 102. Формальная модель программы

После grounding и normalization программа состоит из:

```text
F+    positive asserted literals
F-    explicit negative asserted literals
Rs    strict rules
Rd    defeasible rules
Rx    defeaters
Pr    priority rules
```

Ground literal имеет complement:

```text
complement(P(args))     = not P(args)
complement(not P(args)) = P(args)
```

## 103. Strict closure

Strict closure вычисляется как наименьшая неподвижная точка strict rules над accepted prerequisites. Positive recursion strict rules разрешена. Цикл без base fact ничего не выводит.

Strict conflict не приводит к explosion. Поскольку bare atom является status-sensitive (`TRUE_ONLY`), recursive strict definitions должны использовать монотонное ребро — канонически `monotone(P)` (§65, errata E-0018; принадлежит L0). Например, transitive closure рекурсирует через `monotone(ancestor(...))`. `supported(P)` несёт тот же тест и как ребро цикла равнозначен, но принадлежит L3 (потребление конфликта) — писать рекурсию через него значит поднимать слой программы без нужды. Cycle через bare/`established` остаётся запрещённым status cycle.

## 104. Defeasible candidate

Ground application defeasible rule является candidate, если:

1. rule applicable по source/time/context;
2. body имеет result `TRUE_ONLY`;
3. все external dependencies разрешены;
4. selected interpretation включает rule.

Ground application defeater является attacking candidate при тех же условиях.

## 105. Opposition

Две applications противоположны, если их heads являются complements после grounding. Normative positions противопоставляются через standard conflict predicates профиля, например:

```text
duty(actor, perform(A))
```

против:

```text
duty(actor, forbear(A))
```

или explicit prohibition против explicit liberty. Core standard library задаёт базовые norm-conflict relations; jurisdiction profile может добавлять более сложные.

## 105.1. Базовые normative conflict patterns

Core standard library признаёт conflict только при совместимом grounding субъектов и пересекающемся temporal scope:

1. две duties одного bearer конфликтуют, если solver или explicit relation доказывает, что их goals нельзя совместно выполнить;
2. duty-forbearance и liberty совершить тот же action конфликтуют при совпадающем holder/bearer и релевантном `against` scope;
3. duty-achievement и liberty не совершать несовместимое действие конфликтуют только при доказанной incompatibility;
4. power создать effect `E` и immunity от соответствующего effect `E` образуют conflict pair;
5. две powers сами по себе не конфликтуют, пока их effects не доказаны несовместимыми;
6. две liberties сами по себе не конфликтуют;
7. duty и claim-right являются двумя views одной позиции и не считаются конфликтом.

Goal incompatibility НЕ выводится по различию текста или количеству условий. Она устанавливается pure constraint solver-ом в decidable fragment, explicit `incompatible(...)` relation либо jurisdiction interpretation. Если несовместимость только возможна, analyzer сообщает `POSSIBLE_NORM_CONFLICT`, но evaluator не создаёт defeat edge.


Solver-assisted incompatibility может влиять на legal defeat только если EvaluationInputManifest pin-ит `solver_profile` (logic, arithmetic semantics, timeout-independent proof format) и proof graph содержит independently checkable certificate. `SAT/UNSAT` без certificate либо timeout считается `UNKNOWN` и не создаёт conflict/priority edge. Heuristic/ML classifier может дать warning, но не semantic conclusion.

### 105.2. Обнаружение и разрешение конфликта позиций

Образцы §105.1 — утверждение о том, ЧТО является конфликтом. Здесь — как он
обнаруживается, чем доказывается несовместимость и что происходит дальше.
Пункт 4 (power против immunity) реализован материализацией эффекта §127.2 и
этой процедурой не затрагивается: его стороны — не две позиции, а позиция и
эффект.

**Пара рассматривается только при совместимом grounding субъектов.** Носитель
обязанности и держатель свободы обязаны быть ОДНИМ ground-термом; пары с
разными субъектами не образуют конфликта ни при какой несовместимости целей.
Temporal scope обязан пересекаться: окна §124 двух позиций, не имеющие общей
точки, конфликта не дают — норма, истёкшая до начала другой, ей не
противоречит.

**Три источника несовместимости, и порядок между ними — старшинства, а не
предпочтения.**

1. **Структурный** — пункт 2 §105.1. Обязанность воздержания (`goal
   forbearance` с полем `action`) и свобода совершить ТОТ ЖЕ action при
   совпадающем субъекте конфликтуют БЕЗ всякого доказательства: доказывать
   нечего, несовместимость есть тождество действия. Если у свободы объявлен
   `against`, он обязан покрывать носителя обязанности.
2. **Явное отношение** — `urn:law:std#incompatible(A, B)`, где `A` и `B` —
   ссылки на норм-ШАБЛОНЫ (§122), а не на позиции: несовместимость есть
   свойство целей, а цели живут в шаблоне. Отношение читается из store как
   обычный установленный литерал, поэтому его вправе поставить и дело, и
   правило акта, и толкование §152.
3. **Solver-assisted** — только по правилам абзаца выше: `solverProfile` в
   манифесте И проверяемый сертификат. Сертификат ПЕРЕПРОВЕРЯЕТСЯ движком, а
   не принимается на веру. Профиль `law.solver.finite-enumeration/0.1` задаёт
   его форму и разрешимый фрагмент: цели обеих позиций суть положительные
   ground-литералы ОДНОГО предиката, у которого объявлен ключ §45.1;
   сертификат называет предикат, ключевые позиции и столбцы, в которых
   аргументы разошлись. Утверждение сертификата — «ключ совпал, значение
   разошлось», то есть перечисление домена ключа даёт ноль присвоений,
   удовлетворяющих обе цели: функциональная зависимость §45.1 запрещает
   второе значение при том же ключе. Движок повторяет ровно это сравнение;
   расхождение делает сертификат недействительным. Всё вне фрагмента —
   отсутствие профиля, отсутствие сертификата, цели разных предикатов,
   предикат без ключа, совпадение по всем неключевым столбцам — даёт
   `UNKNOWN` и НЕ создаёт ребра.

Jurisdiction interpretation как четвёртый источник §105.1 называет, но
механизм профиля правопорядка в v1 не определён; источник объявлен и не
реализован.

**Возможная несовместимость — не несовместимость.** Если ни один источник не
дал доказательства, но статический анализ считает конфликт возможным,
выпускается `POSSIBLE_NORM_CONFLICT` (severity warning), и ребра не
создаётся. Читать это предупреждение как конфликт запрещено: §105.1 говорит
«evaluator не создаёт defeat edge» дословно.

**Разрешение — §106 и §107, без нового механизма.** Доказанный конфликт делает
два производящих применения противоположными кандидатами. Дальше:

- приоритет разрешает пару (`r ≻ s`) — проигравшее применение побеждено, и
  его позиция получает статус `DEFEATED` (§134.1) с узлом `defeat` в
  proof-графе, ровно как при дефитере §107.1;
- приоритета нет либо стороны несравнимы — выпускается
  `UNRESOLVED_NORMATIVE_CONFLICT` (severity warning), и ОБЕ позиции остаются.
  Случайного tie-break не делается (§106 запрещает его дословно), и ни одна
  из сторон не объявляется победившей молча.

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

Результат запроса `positions`, в котором остался неразрешённый конфликт,
несёт `evaluation_status = UNRESOLVED_NORMATIVE_CONFLICT` (§25 перечисляет
этот статус, §18 требует его у transformation query при непобеждённой паре
Power/Immunity). Ответ обязан называть конфликт САМ: `COMPUTED` на паре
несовместимых позиций читается как «право посчитано», тогда как право
столкнулось и не разошлось, а issues документа спрашивающий через MCP или
рабочий стол не видит.

## 106. Priority relation

`A ≻ B` означает, что application A сильнее application B в данном Context.

Priority является strict partial order в executable evaluation:

- irreflexive;
- transitive;
- acyclic.

Evaluator вычисляет context-specific transitive closure. Отсутствие пути между двумя applications означает incomparability, а не равенство.

Если context-dependent priority создаёт cycle, affected conflict group получает `PRIORITY_CONFLICT`; evaluator не использует случайный tie-break.

## 107. Defeat

Candidate `r` для conclusion `q` побеждён, если существует applicable opposing candidate `s` и выполняется одно из условий:

1. `s` strict, а `r` defeasible;
2. `s` является ordinary contrary defeasible candidate и `s ≻ r`;
3. `s` является defeater, направленным на `q`, и НЕ установлено `r ≻ s`.

Таким образом, explicit defeater блокирует равный или несравнимый defeasible candidate, но более сильное правило может преодолеть defeater. Generated `unless` дополнительно создаёт direct priority exception over general rule. Defeasible candidate никогда не побеждает strict support.

Гарантия п. 1 опирается на барьер §110 п. 5: strict support противника обязана быть готова к построению conflict group вывода `q`. Строгий противник, чьё тело достижимо от эффекта полномочия §127, этого условия не выполняет — эффект материализуется после всех strata (§280.3), — и потому отклоняется как поздний производитель (§111, errata E-0238), а не оставляет в документе одновременно выживший defeasible-вывод и строгую опору комплемента (`BOTH` §108).

Defeat АДРЕСЕН: побеждается candidate НАЗВАННОГО вывода `q`, а `q` цели
`defeat R(…)` есть один ground-литерал после подстановки. Отсюда граница, о
которой обязана предупреждать реализация. Если хотя бы один аргумент цели —
величина (вычисление прямо в цели либо переменная типа `Date`, `Instant`,
`Money`, `Quantity`, `Decimal`, `Rational`, `Integer`) И у предиката цели два
и более ПОРАЖАЕМЫХ производителя, то дефитер снимает опору не «своей» нормы,
а всякой, чей вывод совпал значением, — включая ту, о которой он ничего не
сказал. Результат при этом пуст, промежуточные отношения стоят, ни одного
issue не рождается. Форма диагностируется warning `LDC-E2144` (DECISION-0352
§2); уровень — предупреждение, потому что запись бывает намеренным чтением
источника. Рабочая форма — беззначное отношение применимости между нормой и
результатом (DECISION-0344 §4): отменяется ПРИМЕНИМОСТЬ, а не литерал с
числом. Единственный производитель и строгий производитель в форму не входят:
в первом случае вытеснять нечего, во втором §107 п. 1 отдаёт победу строгой
опоре при любом совпадении значений.

### 107.1. Defeat вывода-НОРМЫ

`q` в §107 не ограничен литералом: заключением defeasible candidate может быть
норм-шаблон (§122–§124), и тогда побеждается ground application, выводящее
позицию. Это тот же §107, а не отдельный механизм: `s` обязан быть applicable
opposing candidate, и три условия победы читаются дословно.

Соответствие «то же `q`» у норм-заключения устанавливается ПАРОЙ, а не одним
признаком: тот же norm template И совпадение подстановки на переменных,
входящих в payload шаблона. Переменные тела общего правила, в payload не
попавшие, соответствия не образуют — иначе дефитер, связавший лишь посылку,
побеждал бы позиции, о которых ничего не сказал. Требование §190 к
порождённому узлу при этом уже действует и здесь: каждая переменная payload
обязана быть связана позитивным established-конъюнктом самого `C` (§149.1),
и невыполнение даёт `LDC-E4101` на имя `<rule>/unless/N`.

Побеждённое application позиции НЕ создаёт: по §108 у вывода без выжившего
кандидата нет accepted support. Сама позиция при этом остаётся видимой в
результате со статусом `DEFEATED` (§134.1), а её статусные literals не
публикуются — видимость ответа и участие в выводе здесь расходятся намеренно.

Контрарная форма `unless C then not A` при норм-голове НЕ определена и обязана
отвергаться: `not A` требует комплемента заключения, а комплемента у позиции
нет — противопоставление позиций идёт образцами §105.1, а не отрицанием
шаблона. Реализация отвечает статической ошибкой, а не молчаливым отбросом.

Деонтический конфликт ДВУХ позиций (§105.1) этим не затрагивается: там
противопоставляются два вывода, здесь — вывод и направленный на него
дефитер.

## 108. Surviving support

`q` получает accepted defeasible support, если существует хотя бы один applicable candidate для `q`, который не побеждён.

Если у `q` и complement `q` остаются surviving candidates, TruthStatus становится `BOTH`.

Не используется неявный принцип «последнее правило побеждает» или «первое правило побеждает».

## 109. Team support

0.1 использует candidate-level team behavior:

- каждый candidate оценивается отдельно;
- conclusion выживает, если выжил хотя бы один candidate;
- слабый candidate не портит более сильный candidate той же стороны;
- proof graph показывает, какие именно applications были побеждены.

## 110. Stratification

Для масштабируемой и детерминированной реализации строится dependency graph.

Edges:

- `strict-positive` — strict rule зависит от positive support (сюда же — монотонные рёбра `monotone(P)` / `supported(P)`);
- `defeasible` — defeasible conclusion зависит от body predicate;
- `status` — зависимость через `established`, `conflicted`, `unknown`, bare atom; status test условного терма §56 в голове или теле даёт это ребро (`default` для `not_known`/`unknown`) при любой обёртке, `supported`/`monotone` тоже (errata E-0176, E-0177);
- `default` — зависимость через `not_known`;
- `priority` — priority expression зависит от predicate/metadata;
- `completion` (errata E-0112) — читатель ПЕРЕЧИСЛЯЕТ выводимый предикат целиком: generator comprehension §52.1 под агрегатом §59 или доменом квантора §52, в теле либо в голове. Обёртка `monotone(P)`/`supported(P)` вид ребра не меняет: точечный тест опоры монотонен, перечисление множества — нет. Читатель стоит строго выше всех производителей обеих полярностей `P`. Изъятие — монотонный агрегатный гард §111 (errata E-0116).

`core-executable` требует:

1. cycles могут содержать только `strict-positive` edges;
2. cycle с `defeasible`, `status`, `default`, `priority` или `completion` edge запрещён;
   цикл длины один — тоже цикл (errata E-0173): defeasible-правило или дефитер,
   читающие в теле собственную голову любым чтением (голым атомом,
   `monotone(P)`/`supported(P)`, под квантором или монотонным агрегатным
   гардом), дают `NON_EXECUTABLE_UNSTRATIFIED`, как и цикл из нескольких
   поражаемых правил. Каждое чтение тела поражаемого правила — ребро вида
   `defeasible`, в том числе там, где ранг читателя от производителя не
   поднимается. Выравнивание дефитера по атакуемой голове (п. 5) чтением
   тела не является и цикла не образует.
   Условие клаузы `unless` / `except_when` §149/§150 — ТЕЛО порождённого ею
   узла (голая клауза — дефитер по голове правила, контрарная `unless … then P`
   — поражаемое правило с головой `P`), и его чтения дают те же рёбра, что
   чтения `when`: форма записи на нормализацию не влияет (errata E-0211).
   Цикл, замкнутый такими чтениями, compiler обязан находить СТАТИЧЕСКИ —
   `LDC-E4102`, и диагностика называет адреса правил цикла вместе с
   порождёнными узлами `<Правило>/unless/N`. Граница проверки — ОДИН пакет:
   §27.3 собирает все его файлы в одну программу до статик, поэтому цикл
   внутри пакета обязателен к обнаружению, а цикл, замыкающийся через правила
   ИМПОРТИРОВАННОГО пакета, статикой 0.2 не покрыт — resolve-контекст §24
   несёт имена и виды публичных символов, а не тела чужих правил.
   `NON_EXECUTABLE_UNSTRATIFIED` у evaluator-а остаётся страховкой для миров,
   собранных мимо компилятора, и единственным каналом для цикла через импорт;
3. priority expression не зависит от conclusion conflict group, которую он разрешает;
4. negation/default strata конечны;
5. **все потенциальные producers обеих полярностей одной головы, включая
   дефитеры, стоят у одного completion barrier** (errata E-0080, 0.2-01): ранг
   правила не меньше максимума рангов всех правил, чья голова — тот же
   предикат. Дефитер выравнивается по обычным defeasible-продюсерам именно той
   полярности, которую атакует. Если такого кандидата нет, выравнивание
   невозможно: compiler отклоняет источник как `LDC-E4112
   DEFEATER_WITHOUT_CANDIDATE`, а evaluator отвергает вручную собранный CLIR как
   `NON_EXECUTABLE_STRATUM_BARRIER`; strict-вывод и empirical assertion
   defeasible-кандидатами не становятся (§107.3). Без этого шага 7 §111 фиксировал бы TruthStatus атома в
   нижней страте, пока производитель той же головы в верхней ещё не отработал,
   а дефитер до нижней страты не доходил бы вовсе — поражение не применялось бы
   НИ РАЗУ и молча (см. E-0080: четыре живых пакета корпуса, у одного неверный
   ответ на исполнении). Выравнивание вычисляется внутри того же фикспойнта,
   что и ранги: подъём правила поднимает его потребителей, а те —
   производителей своих голов; программа, у которой фикспойнт не сходится,
   по-прежнему даёт `NON_EXECUTABLE_UNSTRATIFIED`.
   Производители предиката — не только правила с его головой (errata E-0172).
   Строгое правило, чьё тело или scope читает поражаемо выводимый предикат
   положительным конъюнктом (голым атомом или `established`, `supported`,
   `monotone`), продолжает поражаемый вывод строго-позитивной цепочкой.
   Strict closure повторяется шагом 1 каждой следующей страты (§111), поэтому
   голова такого правила и всё, что строго выводится из неё дальше, полны
   только после страты своего поражаемого источника. Поражаемое правило или
   дефитер, читающие такой предикат в теле любым чтением либо выводящие его
   голову, стоят строго выше самой высокой страты источников цепочки.
   Эффект полномочия §127 производителем предиката тоже является, но ранга
   у него нет: выравнивание строгого правила, которое читает эффект-достижимый
   предикат и выводит комплемент головы defeasible-кандидата, недостижимо, и
   такое правило отклоняется (§111, errata E-0238).

Representation profile может хранить unstratified theory, но evaluator возвращает `NON_EXECUTABLE_UNSTRATIFIED`.

## 111. Порядок evaluation strata

Для каждого stratum:

Точечное чтение `monotone(P)`/`supported(P)` конъюнктом — ребро монотонной рекурсии §103 и остаётся внутри strict-LFP. Перечисление выводимого предиката — generator comprehension §52.1 для агрегата §59 или домена квантора §52 — есть ребро `completion` §110 (errata E-0112): значение `count`/`sum`/`min`/`max`, истинность `forall` по растущему домену и сама полнота comprehension не монотонны, и обёртка `monotone` этого не меняет. Производители предиката завершают свой least fixed point, затем потребитель исполняется один раз над замороженным множеством; цикл через `completion` не стратифицируем (`LDC-E4102`, `NON_EXECUTABLE_UNSTRATIFIED`). Изъятие (errata E-0116) — МОНОТОННЫЙ АГРЕГАТНЫЙ ГАРД: позитивный конъюнкт тела `AGG(collect v … where G) OP c`, где пара `AGG`/`OP` — `count`/`sum`/`max` против нижней границы (`>=`, `>`) либо `min` против верхней (`<=`, `<`); `c` сам ничего не перечисляет; `G` читает выводимые предикаты ТОЛЬКО через `monotone(P)`/`supported(P)` §65, а невыводимые — положительным `established`. Такой тест не убывает с ростом множества, поэтому его generator-чтения — рёбра `monotone`, читатель стоит в страте производителей, и правило допускается к повтору на той же подстановке, пока гард не выполнен (ключ идемпотентности ставится только при срабатывании). Обратные пары (`count`/`sum`/`max` против верхней границы, `min` против нижней), `average`, агрегат в ГОЛОВЕ и домен квантора остаются `completion`. Для `sum` монотонность держится на неотрицательности слагаемых, а знака статика не видит: отрицательное слагаемое под монотонным гардом — evaluation error `MONOTONE_GUARD_NEGATIVE_ADDEND` (error, адрес правила), и правило на этой подстановке не срабатывает. Требовать конъюнкт знака в самом generator-е нельзя: он меняет каноническое тело §206 и вместе с ним порядок конъюнктов. Строгое правило, перечисляющее предикат с ПОРАЖАЕМЫМИ производителями, — `NON_EXECUTABLE_RULE`: страты строгого слоя производителей L1 не видят, норма пишется поражаемым правилом. До errata абзац разрешал generator «через `monotone(P)`», реализации клали читателя в страту производителей, и агрегат в голове считался при первом срабатывании по недособранному множеству — при зелёных `check`, `lower` и differential. Bare/`established`, default и отрицательные чтения остаются completion barrier, как прежде.

**Issue монотонного агрегатного гарда предъявляется по НЕПОДВИЖНОЙ ТОЧКЕ, а не по промежуточному раунду (errata E-0198).** Раз правило с таким гардом стоит в страте своих производителей и повторяется, пока гард не выполнен, то состояние коллекции в промежуточном раунде — не итог, а ход вычисления: в первом раунде выводимый предикат ещё пуст, comprehension законно даёт пустую коллекцию, и `EMPTY_AGGREGATE` §59 над ней говорит «правило пока не сработало», а не «вычисление отказало». Поэтому issue ошибки вычисления терма §58, выпущенная ПРОВЕРКОЙ монотонного агрегатного гарда, предъявляется по состоянию неподвижной точки той страты, в которой правило стоит; закрытие страты производителей для такого гарда и есть достижение этой неподвижной точки, потому что производители стоят в ней же. Ошибка промежуточного раунда, не повторившаяся на последнем (том, который не добавил ни одного вывода), в документ не попадает; ошибка, впервые зазвучавшая на последнем раунде, предъявляется наравне с ошибкой первого. На закрытой страте пустая коллекция предъявляется как всегда: тот же код, тот же текст, уровень `error`, адрес правила. Правило общее по коду — удерживается любая ошибка проверки такого гарда, ибо её вход растёт вместе с множеством, — и узкое по месту: ошибка вычисления головы, аргумента тела, квантора и `MONOTONE_GUARD_NEGATIVE_ADDEND` (он считается по подстановке уже после успешной проверки гарда) не удерживаются, их вход внутри страты не растёт. Удержание касается только гарда, чья коллекция внутри страты РАСТЁТ, то есть чей generator читает выводимый предикат через `monotone(P)`/`supported(P)`: у гарда над одной эмпирикой коллекция заморожена входом дела и первый раунд равен неподвижной точке. Порядок issue остаётся детерминированным: удержанные ошибки страты предъявляются при её закрытии одной группой в порядке правил страты, а страты закрываются по очереди. Proof-граф не затрагивается: правило, чей гард отказал, на этом раунде не применяется вовсе, и применений промежуточных раундов в графе нет. Удержание предшествует total outcome §181.2: гасит документ то, что предъявлено по неподвижной точке.

1. вычислить strict least fixed point;
2. вычислить bodies defeasible/defeater applications;
3. построить conflict groups;
4. вычислить priority relation;
5. отметить defeated candidates;
6. добавить surviving supports;
7. зафиксировать TruthStatus predicate instances;
8. перейти к следующему stratum.

Так как status-sensitive consumers находятся выше producers, поздний конфликт не отзывает уже использованный lower-stratum status. Барьер относится и к producers САМОГО предиката: шаг 7 фиксирует TruthStatus, когда отработали ВСЕ правила его головы, а не только правила текущей страты, — это обеспечивается требованием 5 §110 (errata E-0080, 0.2-01). Для этого compiler строит **predicate completion barrier**: все потенциальные producers обеих полярностей `P`/`not P`, включая атакующие их дефитеры, должны завершиться до построения conflict groups и до первого `established/conflicted/unknown/not_known` consumer. Дефитер без обычного defeasible-кандидата той же полярности отклоняется, потому что §107.3 не даёт ему объекта поражения; разрыв не исправляется вторым проходом. Обнаруженный late producer является `LDC-E4103 LATE_STATUS_PRODUCER`, а не разрешается порядком файлов.

**Строгая цепочка над поражаемым выводом — тоже производитель** (errata E-0172). Барьер охватывает не только правила головы `P`, но и строгие правила, выводящие `P` строго-позитивной цепочкой (§110 п. 5) из головы поражаемого правила страты `k`. Strict least fixed point страты `k` исполняется шагом 1 ДО кандидатов этой страты, а их опоры приходят шагом 6, поэтому такой `P` полон только к шагу 1 страты `k + 1`. Отсюда два следствия, одинаковые для прямого и цепочного производителя. Первое: поражаемый читатель `P` и поражаемый производитель головы `P` поднимаются ранг выше источника цепочки; это подъём ранга, а не отказ, и правило исполняется. Второе: строгий читатель, для которого положение выше источника недостижимо, отклоняется. Это `not_known(P)`, перечисление `P` (generator агрегата §59 или домен квантора §52) и условный терм §56 в голове или теле над опорой `P` (errata E-0176, E-0177): `LDC-E4103 LATE_STATUS_PRODUCER` у compiler-а, `NON_EXECUTABLE_RULE` с пропуском правила у evaluator-а на рукописном CLIR, тем же порядком, что у чтения над прямым поражаемым производителем (DECISION-0088). Цепочка продолжается только строгими правилами: поражаемое правило, читающее `P`, само становится производителем своей головы со своим рангом. До errata обе реализации смотрели только на прямого поражаемого производителя. Поражаемый читатель вставал в страту источника и терял вывод (`q ⇐d a`, `p ⇐s monotone(q)`, `r ⇐d p` — `r` NEITHER вместо TRUE_ONLY) либо сохранял умолчание (`r ⇐d b ∧ not_known(p)` — TRUE_ONLY вместо NEITHER), а строгое `not_known(p)` вычислялось до вывода `p` и не отзывалось.

**Свёртка истории §161.1 как граница страт** (DECISION-0156 §2.4, errata E-0142). Свёртка вставляется между завершёнными стратами. Разбиение сохраняет predicate completion barriers обеих полярностей и полноту разрешения конфликтов; зависимости условий приоритета учитываются наравне с чтениями правил. Strict-замыкания и замыкания §70 согласуются с тем же планом. Промежуточные кандидаты не являются входом свёртки. Физическое число проходов не изменяет семантику группы и полноту её сертификата.

Отсюда три следствия, обязательные для реализации. Первое: страта L1 не делится по СИЛЕ правила — она делится по ГРУППЕ предиката, и группа, часть производителей которой стоит выше свёртки, стоит выше целиком. Второе: подготовка слоя (кандидаты, замыкание приоритетов §106, ранги §110) считается по ПОЛНОЙ программе, а исполняемые группы отбираются планом; иначе транзитивное ребро приоритета, проходящее через правило выше свёртки, исчезло бы в нижней части, и положение фазы изменило бы решётку §106. Третье: пространство идентификаторов proof (`defeat`, `closure`, конфликтные отчёты §115) — ОДНО на вызов, а не на физический проход; сертификаты §181.1 обеих частей несут исходные `programHash`/`caseHash`, статические issues подготовки предъявляются однократно, а отчёты §115 обеих частей объединяются в один перечень документа.

Эффект полномочия §127 — ПОЗДНИЙ ПРОИЗВОДИТЕЛЬ ПО ПОСТРОЕНИЮ (errata E-0134): `effect create(P)` даёт позитивную опору `P`, но материализуется norm runtime §280.3 после всех strata §280.2, и strict least fixed point повторяется над ним итерациями §143 — строгие `established`-читатели `P` и предикатов, выводимых из него строго, видят эффект в том же документе (§143.1), а status-sensitive читатели — нет: `not_known`/`unknown`/`refuted` над таким предикатом уже вычислены по снимку без эффекта, и их вывод append-only не отзывается. Для барьера этого абзаца эффект считается производителем `P` и всех предикатов, достижимых от `P` строго-позитивными рёбрами (`established`/bare, `supported`/`monotone`); в графе §110 рёбром он НЕ является (§143.1: цикл через эффект — штатное субделегирование). Строгое правило со status-sensitive чтением такого предиката (`not_known`/`unknown`/`refuted` в теле, условный терм §56 в голове или теле — errata E-0176, E-0177) отклоняется: compiler — `LDC-E4103 LATE_STATUS_PRODUCER`, evaluator на рукописном CLIR — `NON_EXECUTABLE_RULE` с пропуском правила, тем же порядком, что у чтения над поражаемым производителем (DECISION-0088). Поражаемые читатели §104 таких предикатов в 0.2 после материализации не повторяются (DECISION-0021 §4.3) — это названный остаток до локальной стратификации по индексу тура (§111.1, LAYERS-NEXT С-4), где эффект становится производителем тура, а не поздним.

**Строгий противник поражаемого вывода от эффекта — тот же поздний производитель** (errata E-0238). Строгое правило, голова которого — КОМПЛЕМЕНТ головы обычного defeasible-кандидата §104 (кандидат выводит `q`, правило — `not q`, или наоборот), а тело или scope читает положительным конъюнктом (голым атомом, `established`, `supported`, `monotone`) предикат, достижимый от эффекта полномочия в смысле предыдущего абзаца, — производитель `q` у barrier §110 п. 5, которого барьер не видит. Без отказа conflict group `q` строилась бы без него, выживший defeasible-кандидат фиксировал TruthStatus шагом 7 этой страты, а строгая опора, пришедшая итерацией §143, добавлялась бы рядом append-only: документ отвечал бы `BOTH` §108 при строгой опоре комплемента, то есть опровергал бы §107 п. 1 внутри себя. Поэтому такое правило отклоняется тем же порядком, что status-sensitive чтение эффект-достижимого предиката: compiler — `LDC-E4103 LATE_STATUS_PRODUCER`, evaluator на рукописном CLIR — `NON_EXECUTABLE_RULE` с пропуском правила. Строгое правило над эффект-достижимым телом, голова которого не противоположна ни одному defeasible-кандидату, исполняется как прежде (§143.1): опора той же полярности, что у кандидатов, комплемента не создаёт, а дефитер §107 п. 3 вывода не утверждает. Формы автора две. Если право отпадает по наступлению события или истечению срока, отпадение пишется строгим конститутивным правилом над эмпирическими фактами дела, а не эффектом полномочия: тогда противник — обычный строгий производитель, и поражение §107 п. 1 происходит в той же страте. Если отпадение действительно есть осуществление чужого полномочия, поражаемое право само записывается позицией `power` (§127) с прекращением по §135–§138, и о нём спрашивают запросом `positions`, а не `truth`.

### 111.1. `stage` — зарезервированная граница 0.2

`stage Name {}` — именованная декларация `law.core/0.2`, заранее
резервирующая узел CLIR для локальной стратификации по индексу тура. В 0.2
тело обязано быть пустым, а узел имеет `kind: "stage"` и `status:
"reserved"`. Декларация входит в обе идентичности программы как обычный узел.

Ни номера тура, ни порядка индекса, ни исполнения тела в 0.2 нет. Наличие
узла `stage` в поданной программе останавливает evaluation до вывода с fatal
issue `NON_EXECUTABLE_STAGE`, пустыми `results` и `proofGraph.roots`. Это
громкая граница, а не no-op. Локальная стратификация `Integer`/`Date` и
семантика тела относятся к 0.3 (LAYERS-NEXT С-4).

## 112. Ambiguity policy

Core 0.1 является ambiguity-preserving:

- incomparable candidates не побеждают друг друга;
- обе стороны остаются поддержанными;
- bare conditions в следующих strata не считают `BOTH` установленным;
- explicit `supported(P)` может использовать одну сторону конфликта;
- query может выбрать skeptical view (`TRUE_ONLY` only) или support view.

Профиль или context МОЖЕТ дополнительно закрепить политику `on_accepted_conflict = halt` (errata E-0001): при обнаружении одновременного accepted positive и accepted negative support одного ground literal evaluation останавливается **до** начала вывода со статусом `CONFLICTED_INPUTS` (§175), не порождая четырёхзначных результатов. Политика семантически активна и входит в EvaluationInputManifest; она предназначена для ограниченных профилей (например, семантический слой L0 по LAYERS-SURFACES §2.3), где конфликт входов является ошибкой данных, а не предметом вывода. Default Core — ambiguity preservation, описанный выше.

## 113. Default negation

`not_known(P)` проверяется только после окончательного вычисления producer stratum. Поэтому:

```text
A if not_known B
B if not_known A
```

не проходит executable validation.

Замыкание §70 — тоже producer stratum: оно производит `not P`. Строгое `not_known(not P)` над закрытым `P` и строгое `not_known(Q)`, где опору `Q` даёт строгий производитель, читающий негатив замыкания, исполняются после материализации замыкания (§70, errata E-0174). Это подъём, а не отказ.

Строгое `not_known(P)` над предикатом, который строгая цепочка выводит из поражаемого вывода, отклоняется так же, как над предикатом с поражаемым производителем (§111, errata E-0172). Поражаемый читатель такого `P` исполняется стратой выше источника цепочки.

Производитель «producer stratum» — не только правило. Эффект полномочия §127 материализуется после всех strata (§280.3) и поэтому для `not_known` есть поздний производитель (§111, errata E-0134): строгое `not_known(P)` над предикатом, достижимым от головы эффекта строго-позитивной цепочкой, не проходит executable validation в 0.2 — `LDC-E4103` у compiler-а, `NON_EXECUTABLE_RULE` у evaluator-а. Форма «умолчание, которое видит эффект того же дела» (default deny при делегированной роли) — предмет локальной стратификации §111.1; до неё умолчание пишется поражаемым правилом либо эффект подаётся вторым делом фактом.

## 114. Strict и legal priority

`strict` — логическая категория, а не юридический ранг источника. Lex superior/specialis/posterior обычно моделируются priority между defeasible legal rules. Нельзя сделать rule strict только потому, что его источник выше в иерархии.

## 115. Конфликтный результат

Conflict report содержит:

```text
conflict_id
positive_literal
negative_literal
positive_candidates
negative_candidates
defeated_candidates
priority_edges
unresolved_reason
source_anchors
interpretations
```

**Форма `conflict_id` (errata E-0246).** `urn:conflict:<хвост>:<sha256>`, где
`<хвост>` — часть StableId предиката положительного литерала после `#`, а
`<sha256>` — шестнадцатеричный SHA-256 канонических байтов §208 отчёта без
поля `id`. Кандидаты в отчёте названы каноническими id §180.1, поэтому хэш
считается после канонизации графа. Порядкового номера у отчёта нет:
отчёт одного и того же конфликта получает один и тот же id при любом
порядке групп, любом разбиении слоя L1 (§111) и в подпрограмме конуса
§181.3. Результат ссылается на отчёт этим id. Форма действует во всех
версиях семантики.

---