# Формальная спецификация MRB-0

## 1. Нормативная область

MRB-0 — типизированное исчисление над JSON-записями. Оно не определяет истинность, референцию, существование, событие, наблюдение или цель вне собственных полей. Слова в payload не меняют тип суждения.

Теорема относится ко всем proof-object, которые принимает точный контракт \(\mathcal C\), заданный ниже.

## 2. Формы суждений

Каждое суждение имеет четыре поля:

~~~json
{
  "kind": "M",
  "payload": "p",
  "bridge_id": null,
  "goal_id": null
}
~~~

Допустимые kind:

| kind | Роль в MRB-0 | Обязательные идентификаторы |
|---|---|---|
| M | формальное суждение | bridge_id = null, goal_id = null |
| B | запись мостового контракта | bridge_id задан, goal_id = null |
| L | запись связи M-payload с A-payload | bridge_id задан, goal_id = null |
| A | прикладное суждение | bridge_id задан, goal_id = null |
| G | запись целевого контракта | bridge_id = null, goal_id задан |
| V | целевое суждение | bridge_id задан, goal_id задан |

Все payload и идентификаторы — строки. kind является протокольной меткой, а не утверждением о названном payload.

## 3. Proof-object

Proof-object содержит:

- точный contract;
- конечный упорядоченный массив steps;
- conclusion_id.

Каждый step содержит:

~~~json
{
  "step_id": "S0",
  "rule_id": "FORMAL-AXIOM",
  "premise_ids": [],
  "conclusion": {
    "kind": "M",
    "payload": "p",
    "bridge_id": null,
    "goal_id": null
  }
}
~~~

Ссылки могут указывать только на более ранние шаги. Для каждого шага проверяющий вычисляет два множества:

\[
\operatorname{bdeps}(S)\subseteq ID,
\qquad
\operatorname{gdeps}(S)\subseteq ID.
\]

Входной JSON не может сам объявить эти множества. Они вычисляются проверяющим из rule_id, premise_ids и conclusion.

## 4. Правила \(\mathcal C\)

Нормативный proof-contract:

~~~json
{
  "contract_id": "beforeword.typed-bridge.v1",
  "encoding": "utf-8",
  "rule_set": "MRB-0",
  "dependency_policy": "union-no-deletion",
  "statement_kinds": ["M", "B", "L", "A", "G", "V"]
}
~~~

Соответствие JSON Schema проверяет форму объекта. Совместимость требует дополнительно точного равенства всех пяти значений этого блока; структурно полный объект с иными значениями получает INCOMPATIBLE-CONTRACT, а структурно неполный — INVALID-PROOF.

### FORMAL-AXIOM

- premises: 0;
- conclusion.kind: M;
- bdeps = \(\varnothing\);
- gdeps = \(\varnothing\).

### FORMAL-COPY

- premises: ровно 1;
- premise.kind = M;
- conclusion.kind = M;
- payload выхода точно равен payload посылки;
- зависимости выхода равны зависимостям посылки.

### BRIDGE-INPUT

- premises: 0;
- conclusion.kind = B;
- bridge_id задан;
- bdeps = \(\{bridge\_id\}\);
- gdeps = \(\varnothing\).

### LINK-INPUT

- premises: 0;
- conclusion.kind = L;
- payload имеет точную ASCII-форму «source=>target»;
- bridge_id задан;
- bdeps = \(\{bridge\_id\}\).

### BRIDGE-INTRO

- premises: ровно 3 в порядке M, B, L;
- B и L имеют одинаковый bridge_id \(b\);
- payload L равен точной ASCII-конкатенации «M.payload=>A.payload»;
- conclusion.kind = A;
- conclusion.bridge_id = \(b\);
- зависимости — объединение зависимостей посылок; поэтому \(b\in bdeps\).

### GOAL-INPUT

- premises: 0;
- conclusion.kind = G;
- goal_id задан;
- gdeps = \(\{goal\_id\}\).

### GOAL-INTRO

- premises: ровно 2 в порядке A, G;
- conclusion.kind = V;
- bridge_id совпадает с A;
- goal_id совпадает с G;
- payload имеет точную ASCII-форму «A.payload=>status»;
- зависимости — объединение зависимостей посылок.

Других правил нет. Ни одно правило не удаляет зависимости.

## 5. Независимый объект AME

\[
AME_{\mathcal C}
:=
\exists\Pi:
\operatorname{Accepted}_{\mathcal C}(\Pi)
\land
\operatorname{kind}(\operatorname{conclusion}(\Pi))=A
\land
\operatorname{bdeps}(\operatorname{conclusion}(\Pi))=\varnothing.
\]

AME не содержит BeyondRecord и не определён через отрицание факторизации. Его свидетель должен быть конкретным конечным proof-object, который проверяющий принимает.

## 6. Теорема

\[
\boxed{\neg AME_{\mathcal C}}.
\]

**Доказательство.** Рассмотрим последний шаг любого принятого proof-object с заключением kind = A. По таблице правил единственным правилом с таким выходом является BRIDGE-INTRO. Оно требует B и L с одним bridge_id \(b\). Оба входных правила записывают \(b\) в bdeps; BRIDGE-INTRO берёт объединение и ничего не удаляет. Поэтому \(b\) присутствует в bdeps заключения, то есть множество непусто. Противоречие с условием AME. \(\square\)

Эквивалентная индукционная формулировка: для каждого принятого шага S,

\[
\operatorname{kind}(S)=A
\Rightarrow
\operatorname{bdeps}(S)\ne\varnothing.
\]

Проверка proof_checker.py является конечной реализацией правил. Общее доказательство остаётся записанной структурной индукцией; успешные тесты не заменяют квантор по всем proof-object.

## 6.1. Параметрическое усиление MRB-*

Конкретный FORMAL-COPY не является пределом теоремы. Определим класс контрактов \(\mathfrak C_{MRB}\) над конечными append-only трассами более общо.

Контракт \(C\) входит в \(\mathfrak C_{MRB}\), если выполнены все условия:

1. kind создаётся защищённым конструктором правила и хранится отдельно от payload; совпадение байтов payload с сериализованным \(A\)-суждением не меняет kind;
2. внутренние правила произвольны, но имеют сигнатуры \(M^k\to M\) для \(k\ge0\); корневой \(M\)-шаг имеет пустой bdeps, а некорневой наследует точное объединение bdeps только своих \(M\)-посылок;
3. bridge-входы \(s\) создаются отдельными конструкторами, получают \(bdeps(s)=\{\operatorname{bridge\_id}(s)\}\) и не доступны внутреннему \(M\)-правилу как конструкторы;
4. каждый конструктор \(A\) требует ранее зарегистрированный bridge-вход и вносит его id в зависимости;
5. последующие правила берут объединение зависимостей и не удаляют ранее записанные id;
6. ссылки направлены только к более ранним шагам; смены kind, удаления шага и перепривязки ребра нет.

Пусть \(\pi_M(\tau)\) — полная упорядоченная \(M\)-проекция принятой трассы \(\tau\): полные step-records с step_id, rule_id, premise_ids и conclusion. Введём replay-форму автономности:

\[
RAME_C(q\mid\mu)
\iff
\exists\rho\in Runs(C):
\pi_M(\rho)=\mu
\land
Br(\rho)=\varnothing
\land
\exists a\in A_\rho:
payload(a)=q.
\]

Здесь \(Br(\rho)\) — множество зарегистрированных bridge-входов. Определение не упоминает пустой список зависимостей у заключения: оно требует принятую повторную трассу с той же полной \(M\)-проекцией, \(A\)-payload \(q\) и вообще без bridge-регистраций.

### Центральная теорема параметрического bridge-разреза

Для любого \(C\in\mathfrak C_{MRB}\), любой принятой трассы \(\tau\) и любых внутренних правил \(M^k\to M\):

Определим provenance-конус операционно:

\[
\operatorname{Cone}_{Br}(\tau)
:=
\{s\in Steps(\tau):bdeps(s)\ne\varnothing\}.
\]

Поскольку bdeps вычисляется как объединение и не удаляется, это множество содержит bridge-входы и все последующие шаги, унаследовавшие их id. Аналитический разрез

\[
E_{Br}(\tau)
=
\tau\upharpoonright
\left(
Steps(\tau)\setminus\operatorname{Cone}_{Br}(\tau)
\right)
\]

сохраняет \(M\)-проекцию побайтно и не сохраняет ни одного \(A\)-шага:

\[
\pi_M(E_{Br}(\tau))=\pi_M(\tau),
\qquad
A_{E_{Br}(\tau)}=\varnothing,
\qquad
Br(E_{Br}(\tau))=\varnothing.
\]

Если \(a\in A_\tau\), то любое допустимое append-only продолжение сохраняет зарегистрированный bridge id в bdeps\((a)\). Позднее «отмывание» provenance не является допустимым продолжением.

**Доказательство.** Корневой \(M\)-шаг имеет пустой bdeps; внутренний \(M\)-шаг наследует объединение только от \(M\)-посылок. Индукцией bdeps каждого \(M\)-шага пуст, поэтому вся полная \(M\)-проекция остаётся вне provenance-конуса. Каждый \(A\)-шаг добавляет bridge id, поэтому входит в конус. Удаление конуса сохраняет полные \(M\)-step-records, оставляет замкнутые premise-ссылки и устраняет каждый \(A\)-узел. Содержимое и число правил \(M^k\to M\) нигде не использованы. Append-only порядок и union-no-deletion не позволяют удалить уже записанный id. \(\square\)

Из admission-условия немедленно следует:

\[
\forall q\quad\neg RAME_C(q\mid\pi_M(\tau)).
\]

Это следствие type-safety/provenance discipline, а не независимый эмпирический факт и не само по себе «опровержение математики». Содержательный центральный результат — noninterference bridge-разреза: полная внутренняя трасса сохраняется при исчезновении всех \(A\).

Это не распознавание слова bridge. proof_checker.py проверяет конструктор rule_id и kind отдельно от payload. Тест с \(M\)-payload, побайтно изображающим сериализованное \(A\)-суждение, сохраняет статус VALID-FORMAL. Конкретный MRB-0 является одним исполняемым \(C_0\in\mathfrak C_{MRB}\); команда --audit-erasure строит замкнутую сокращённую трассу, повторно исполняет её и хеширует полные \(M\)-step-records. Этот конечный аудит не заменяет общее текстовое доказательство.

## 7. Статусы proof_checker.py

| Статус | Условие |
|---|---|
| VALID-FORMAL | принят conclusion.kind = M |
| VALID-BRIDGE-INPUT | принят conclusion.kind = B |
| VALID-LINK-INPUT | принят conclusion.kind = L |
| VALID-GOAL-INPUT | принят conclusion.kind = G |
| VALID-APPLIED-WITH-BRIDGE | принят conclusion.kind = A и bdeps непусто |
| VALID-GOAL-WITH-DEPENDENCIES | принят conclusion.kind = V, bdeps и gdeps непусты |
| INVALID-PROOF | нарушена структура или точное правило |
| INCOMPATIBLE-CONTRACT | структура читается, но значения контракта не поддержаны |
| NO-AUTONOMOUS-EXPORT-IN-MRB-0 | аудит сигнатур правил подтверждает инвариант \(\neg AME_{\mathcal C}\) |
| BRIDGE-ERASURE-PRESERVES-M-IN-MRB-0 | аналитический разрез удалил все bridge-зависимые шаги, сохранил полную M-проекцию и оставил ноль A |

INVALID-PROOF не означает ложность payload. VALID-APPLIED-WITH-BRIDGE не предъявляет названное payload. Статусы относятся только к proof-object.

## 8. Лемма неидентифицируемости

Пусть \(\rho(k)\) — все и только поля, доступные формальной трассе \(T_{core}\). Пусть \(c(k)\) — extension-код, который \(T_{core}\) не читает. Метапроцедура \(V\) читает всю пару, чтобы проверить равенство \(\rho\) и различие \(c\); \(V\ne T_{core}\).

\[
\operatorname{BeyondRecord}_\rho(c)
\iff
\exists k_0,k_1:
\rho(k_0)=\rho(k_1)
\land
c(k_0)\ne c(k_1).
\]

Определим только функциональное отношение:

\[
\operatorname{TraceDeterminesCode}_K(T_{core},c)
\iff
\exists h:T_{core}(K)\to C\;
\forall k\in K:
c(k)=h(T_{core}(k)).
\]

Если \(T_{core}\) локален относительно \(\rho\), то:

\[
\operatorname{BeyondRecord}_\rho(c)
\Rightarrow
\neg\operatorname{TraceDeterminesCode}_K(T_{core},c).
\]

Это лемма о факторизации кодов. Она не называется доказательством, warrant, entailment или истинностью. AME и эта лемма — разные результаты.

## 9. Контракт парного свидетеля

Поддерживаемый contract:

~~~json
{
  "contract_id": "beforeword.fresh-extension.v2",
  "encoding": "utf-8",
  "unicode_normalization": "none",
  "canonicalization": "bw-cjson-2-python-reference",
  "rho_pointer": "/K/*/core",
  "trace_reads": "core-only",
  "extension_claim_id": "q0",
  "extension_allowed_values": [false, true],
  "extension_constraint": "fresh-unconstrained-boolean",
  "K_scope": "closed-exactly-two"
}
~~~

Для каждого \(k\):

\[
\rho(k):=k.\texttt{core},
\qquad
c(k):=k.\texttt{extension.claim\_value}.
\]

record_id является только индексом \(K\). Он не входит в \(\rho\). extension также не входит в \(\rho\).

Допустимость extension задаётся до пары:

1. claim_id точно равен q0;
2. токен q0 отсутствует во всех строковых полях core;
3. claim_value является JSON boolean;
4. contract заранее разрешает оба и только оба значения false и true.

Поэтому различие не создаётся сменой имени утверждения и не считывается из другого строкового поля core: claim_id один и тот же, меняется разрешённое значение свежего кода.

## 10. Внутренний core пары

Core содержит:

- bytes_hex = 700a;
- utf8_string = «p» плюс LF;
- alphabet = [p];
- atoms = [p];
- axiom p;
- правило copy-record;
- деривацию p → p.

Проверка требует:

1. каждый символ формулы входит в alphabet;
2. каждая формула является объявленным atom;
3. premise совпадает с axiom;
4. FORMAL-COPY имеет один предыдущий вход и точный payload;
5. conclusion_id существует;
6. utf8_string точно равна conclusion formula + LF;
7. bytes_hex точно кодирует utf8_string;
8. core_sha256 равен каноническому хешу;
9. оба core канонически идентичны.

Статус внутренней деривации называется DERIVED-IN-FRESH-CORE. Это минимальная формальная система копирования, а не нетривиальная арифметическая теорема.

## 11. Канонизация bw-cjson-2-python-reference

Нормативной реализацией является функция canonical_bytes в pair_checker.py:

- вход сначала проходит точную структурную проверку;
- запрещены повторённые JSON-ключи;
- запрещены Unicode surrogate code points;
- object keys сортируются Python json.dumps(sort_keys=True);
- ensure_ascii=False;
- separators = (comma, colon) без пробелов;
- allow_nan=False;
- кодировка UTF-8;
- порядок массивов сохраняется;
- Unicode-нормализация не выполняется.

Имя явно указывает на reference implementation. Независимая реализация обязана совпасть с опубликованными тестовыми векторами.

## 12. Статусы pair_checker.py

| Статус | Условие |
|---|---|
| UNVERIFIED | нарушена структура, UTF-8, Unicode scalar constraint, формальный core, хеш или идентичность core |
| INCOMPATIBLE-CONTRACT | полностью читаемая структура называет неподдерживаемый контракт |
| RECORD-DETERMINED | два разрешённых claim_value одинаковы в закрытом \(K\) |
| BEYOND-RECORD | два разрешённых claim_value различны в закрытом \(K\) |

BEYOND-RECORD — имя строкового статуса. Оно устанавливает только:

\[
\rho(k_0)=\rho(k_1)
\land
c(k_0)\ne c(k_1)
\]

для двух перечисленных элементов.

## 13. Максимальная точная формула

> В типизированном исчислении MRB-0 каждое принятое A-суждение содержит хотя бы одну мостовую зависимость; принятого A-proof с пустым bridge_dependencies нет. Отдельно: формальная трасса, читающая только одинаковый core, не определяет различающийся разрешённый extension-код.

Эта строка получает REPORT-CONCLUSION-UNDER-MRB-0 и не расширяется до названного payload.

## 14. Граница адекватности

Теорема \(\neg AME_{\mathcal C}\) квантифицирует по всем и только proof-object, принятым точным контрактом MRB-0. Она является инвариантом этого исчисления.

Применение к иному точному корпусу \(X\) требует предъявленного перевода

\[
\tau_X:X\to MRB\text{-}0,
\]

который сохраняет исходные записи, допустимые шаги, тип заключения и множества зависимостей. Критерий классификации \(M/A\) должен быть зафиксирован до вычисления bridge_dependencies и независимо от желаемого результата аудита. Адекватность \(\tau_X\) проверяется отдельно. Без такого объекта статус применения к \(X\) — APPLICABILITY-UNSPECIFIED. Спецификация не содержит универсальной теоремы, отождествляющей MRB-0 со всеми употреблениями строки «математика».