# МАТЕМАТИКА НЕ ВЫШЛА ИЗ ЗАПИСИ ## Полное отрицание автономного экспорта из формальной записи в MRB-0 и параметрическом классе MRB-* Статус заголовка без подзаголовка: UNBOUNDED-STANDALONE. > Ракета полетела. > Это написано. ## Аннотация Исследование принимает корректный формальный вывод как корректный. Затем задаётся более поздний и более узкий вопрос: существует ли проверяемый proof-object, который из одних формальных суждений получает прикладное суждение при пустом реестре мостовых зависимостей. Для ответа вводится типизированное исчисление MRB-0. Все его элементы остаются точными записями. Суждение \(M(r)\) означает, что запись \(r\) получена по формальным правилам MRB-0. Суждение \(A_b(q)\) означает, что запись \(q\) помещена в прикладной реестр относительно явно записанного моста \(b\). Эти формы различаются протокольным типом; ни одна не предъявляет названное строкой \(r\) или \(q\). Формальные правила имеют только заключения типа \(M\). Единственное правило, вводящее тип \(A\), требует мостовые записи и добавляет их идентификатор в bridge_dependencies. Зависимости далее могут объединяться, но не удаляться. Структурная индукция по proof-object показывает: каждое принятое \(A\)-суждение имеет непустую мостовую зависимость. Следовательно, множество принятых proof-object формы \(\Gamma_M;\varnothing\vdash A(q)\) пусто. Это полное отрицание точно определённого автономного экспорта \(\neg AME_{\mathcal C}\), а не отрицание вычисления или внутреннего формального вывода. Параметрическое усиление MRB-* не зависит от правила копирования p. Оно допускает любой набор внутренних правил \(M^k\to M\). Bridge-разрез сохраняет всю упорядоченную \(M\)-проекцию, но удаляет все \(A\)-шаги, поскольку каждый из них имеет зарегистрированного bridge-предка. Поэтому усложнение внутренней математики само по себе не меняет инвариант provenance. Отдельная лемма неидентифицируемости не использует слово «доказательство» как имя факторизации. Она утверждает только: одна формальная трасса не выбирает между двумя заранее допустимыми мостовыми реестрами, если она их не читает. Машинный свидетель реализует конечный вариант со свежим булевым extension-кодом. Результат применяется к собственным строкам. Заголовок и фразы «математика опровергнута» либо «математика ничего не доказала» не получают статус теоремы без точной области. Итоговая научная строка ограничена MRB-0 и не расширяется до существования, несуществования, события, цели, смысла или отсутствия смысла. --- ## 0. Продолжение авторских «Границ записи» Исходный авторский метод [«Границы записи»](https://beforeword.xyz/research/) задал: - \(W_0\) как предоставленное письменное вхождение; - остановку до обратного переноса более поздней атрибуции; - явные процедуру \(P\) и контракт входа \(I\); - класс \(K(W_0,P,I)\); - вердикты RECORD-DETERMINED, BEYOND-RECORD и PROCEDURE-UNSPECIFIED; - требование точной операции, пары свидетелей либо указания отсутствующей процедуры. Новое ядро делает следующий шаг: 1. строит proof-object с типами суждений и происхождением зависимостей; 2. отделяет формальный тип \(M\), прикладной тип \(A\) и целевой тип \(V\); 3. доказывает обязательность мостовой зависимости для любого \(A\)-заключения; 4. отдельно проверяет неидентифицируемость непрочитанного extension-кода; 5. включает машинный аудит собственных публичных строк. В пакете также записана авторская декларация: новое ядро собрано одним автором до сравнительного картирования. Эта декларация не является посылкой теоремы и не устанавливает внутреннюю историю возникновения наблюдения. ## 1. Неподвижная граница В порядке полей протокола сначала фиксируется вхождение \(W_0\). В последующих полях появляются строки: ~~~text линия знак число формула доказательство математика ракета летит зачем смысл есть смысла нет ~~~ Даже «линия» является строкой классификации. MRB-0 не присваивает ни одной строке отношение к названному, если такого отношения нет в сигнатуре контракта. Граница полярно симметрична. Формы «ракета существует» и «ракета не существует» обе сначала являются записями. Формы «смысл есть» и «смысла нет» также получают один начальный тип. Отрицательная форма не получает привилегии. Историческая строка «математика возникла из языка» не используется как факт о прошлом. Вместо неё задаётся только порядок зависимостей внутри proof-object: \[ \mathsf{record} \prec \mathsf{formal\ typing} \prec \mathsf{derivation} \prec_B \mathsf{application} \prec_G \mathsf{value}. \] Знаки \(\prec_B\) и \(\prec_G\) обозначают наличие записанных зависимостей \(b\) и \(g\), а не историческое время. ## 2. Три протокольных типа Пусть \(\mathcal R\) — множество точных записанных форм. В MRB-0 используются: \[ \mathsf M(r)[P] \] — запись \(r\) получена внутри формального контракта \(F\), а \(P\) содержит её мостовые зависимости; \[ \mathsf A_b(q)[P] \] — запись \(q\) внесена в прикладной реестр по мосту \(b\); \[ \mathsf V_{b,g}(q,s)[P;H] \] — записи \(q\) присвоена целевая строка \(s\) по мосту \(b\) и целевому контракту \(g\). Все \(r,q,b,g,s\in\mathcal R\). Типы \(M,A,V\) — поля аудита, а не названные ими сущности. Критически различаются: \[ \mathsf M(\ulcorner\mathsf A_b(q)\urcorner) \] и \[ \mathsf A_b(q). \] Первое — формальная запись, внутри payload которой написана форма \(A_b(q)\). Второе — суждение протокольного типа \(A\). Правила \[ \mathsf M(\ulcorner J\urcorner)\Rightarrow J \] в MRB-0 нет. Его добавление было бы межтиповым правилом и регистрировалось бы как мост. ## 3. Правила Формальные правила имеют форму \[ \frac{ \mathsf M(r_1)[P_1]\quad\dots\quad\mathsf M(r_n)[P_n] }{ \mathsf M(r)[P_1\cup\dots\cup P_n] }. \] Они возвращают тип \(M\). Они не создают мостовой идентификатор. Мостовые входы записываются отдельно: \[ \mathsf B(b)[\{b\}], \qquad \mathsf L_b(r,q)[\{b\}]. \] Прикладное введение имеет форму \[ \frac{ \mathsf M(r)[P]\quad \mathsf B(b)[\{b\}]\quad \mathsf L_b(r,q)[\{b\}] }{ \mathsf A_b(q)[P\cup\{b\}] }. \] Любое дальнейшее правило сохраняет объединение зависимостей. Правила удаления зависимости в контракте нет. Целевой вход \(G(g)\) и правило типа \(A\to V\) образуют ещё один явно регистрируемый слой. Точная спецификация дана в 01_FORMAL_SPEC_RU.md. ## 4. Независимое определение объекта опровержения Пусть \(\Gamma_M\) содержит только исходные \(M\)-суждения и формальные правила. Множество мостовых зависимостей обозначается \(P\). Автономным экспортом \(M\to A\) в MRB-0 называется конечный proof-object \(\Pi\), для которого проверяющий контракт принимает: \[ \operatorname{Check}_{\mathcal C} \left( \Pi: \Gamma_M;\varnothing \vdash \mathsf A(q) \right)=1. \] Глобальная форма: \[ AME_{\mathcal C} := \exists\Gamma_M,\Pi,q: \operatorname{Check}_{\mathcal C} \left( \Pi: \Gamma_M;\varnothing \vdash \mathsf A(q) \right)=1. \] Это определение не содержит BeyondRecord, истинность, референт, факторизацию или заранее записанное противоречие. Оно спрашивает о существовании конкретного принятого proof-object с типом заключения \(A\) и пустым происхождением моста. AME — техническое имя объекта MRB-0, а не установленное описание каждого употребления слова «математика». ### Условие переноса на математический случай Чтобы применить теорему к конкретной практике, названной строкой «математика», требуется отдельный контракт перевода \(\tau\). Он должен отобразить её точные исходные записи, правила и proof-object в типы и правила MRB-0, сохранив принятие шагов, различие \(M/A/V\) и все зависимости. Критерий классификации \(M/A\) фиксируется до проверки bridge_dependencies и не может зависеть от желаемого вердикта. Только после предъявления и проверки такого \(\tau\) результат переносится на его зафиксированный домен. Без \(\tau\) статус применения — APPLICABILITY-UNSPECIFIED. В этом пакете не доказана одна универсальная \(\tau\), адекватная всем практикам, когда-либо названным словом «математика». Поэтому \(\neg AME_{\mathcal C}\) является полным инвариантом происхождения для MRB-0, а не уже доказанным свойством неограниченного класса под одним именем. ## 5. Теорема обязательной мостовой зависимости ### Теорема Для любого proof-object \(\Pi\), принятого контрактом \(\mathcal C\): \[ \Pi\vdash\mathsf A_b(q)[P] \quad\Rightarrow\quad P\ne\varnothing. \] Следовательно: \[ \boxed{ \Gamma_M;\varnothing \nvdash_{\mathcal C} \mathsf A(q) } \] и \[ \boxed{\neg AME_{\mathcal C}}. \] ### Доказательство Индукция по высоте \(\Pi\). 1. Лист FORMAL-AXIOM имеет тип \(M\), а не \(A\). 2. Каждое формальное правило имеет заключение типа \(M\), поэтому не может быть последним шагом proof-object с заключением \(A\). 3. BRIDGE-INPUT и LINK-INPUT вводят зависимость \(\{b\}\), но сами не имеют типа \(A\). 4. Единственное правило с заключением \(A\), BRIDGE-INTRO, требует \(B(b)\) и \(L_b(r,q)\) и записывает \(b\) в объединение зависимостей. 5. Любое правило, переносящее уже полученное \(A\)-суждение, наследует непустое множество зависимостей и не может его удалить. 6. Других правил с заключением \(A\) в \(\mathcal C\) нет. Поэтому принятого \(A\)-заключения с \(P=\varnothing\) нет. \(\square\) Это структурный инвариант дерева доказательства, а не прежняя тавтология факторизации. ## 5.1. Параметрическая теорема bridge-разреза Пусть \(\mathfrak C_{MRB}\) — класс append-only контрактов, где: - kind создаётся защищённым конструктором, а не распознаётся внутри payload; - внутренние правила произвольны при сигнатуре \(M^k\to M\); корни имеют пустой bdeps, остальные \(M\)-шаги наследуют объединение только от \(M\)-посылок; - каждый bridge-вход \(s\) получает \(bdeps(s)=\{\operatorname{bridge\_id}(s)\}\), а каждый \(A\)-конструктор требует ранее зарегистрированный bridge и сохраняет его id; - зависимости объединяются, но не удаляются; - все ссылки направлены только к более ранним шагам. Для принятой трассы \(\tau\) обозначим её полную упорядоченную математическую проекцию через \(\pi_M(\tau)\); она содержит полные step-records, включая правила и ссылки на посылки. Определим provenance-конус как все и только шаги с непустым bdeps и удалим его. Полученный аналитический разрез \(E_{Br}\) удовлетворяет: \[ \pi_M(E_{Br}(\tau))=\pi_M(\tau), \qquad A_{E_{Br}(\tau)}=\varnothing, \qquad Br(E_{Br}(\tau))=\varnothing. \] Доказательство не читает payload и не использует содержание внутренних правил. Каждый \(M\)-шаг зависит только от \(M\), поэтому сохраняется. Каждый \(A\)-шаг зависит от bridge, поэтому удаляется. Следовательно, результат инвариантен относительно произвольной замены внутреннего исчисления, пока новые правила остаются \(M^k\to M\). Replay-автономность требует принятую трассу с той же полной \(M\)-проекцией, хотя бы одним заданным \(A\)-payload и вообще без bridge-регистраций. Её отрицание непосредственно следует из admission-условия и является следствием type-safety/provenance discipline. Центральный результат — bridge-cut/noninterference: сохранение всей \(M\)-трассы при исчезновении всех \(A\). Точная формула и доказательство даны в §6.1 спецификации. Для каждого MRB-совместимого контракта bridge-разрез сохраняет полную M-проекцию и удаляет все A-шаги. Это не теорема по слову «bridge». В исполняемом MRB-0 строка, побайтно изображающая сериализованное \(A\)-суждение, остаётся \(M\)-payload. Только отдельный rule_id может создать kind = A. Команда --audit-erasure строит и повторно исполняет сокращённую трассу: хеш полных \(M\)-step-records сохраняется, число \(A\) меняется с 1 на 0. ## 6. Почему переименование моста не помогает Если добавить правило \[ \frac{\mathsf M(r)}{\mathsf A(q)}, \] оно классифицируется по сигнатуре \(M\to A\), а не по названию. В MRB-0 это мостовое правило. Названия «аксиома», «очевидность», «математический факт» или «интерпретация» не меняют тип его выхода. Такое правило можно добавить, но тогда получается новый контракт \(\mathcal C'\). Теорема о MRB-0 не переносится на \(\mathcal C'\) автоматически: для него требуется новая проверка сигнатур и происхождения зависимостей. В MRB-0 межтиповой переход регистрирует \(b\). ## 7. Отдельная лемма неидентифицируемости Теорема 5 касается типов и происхождения proof-object. Лемма ниже касается выбора строкового extension-кода и не называется доказательным установлением. Пусть: - \(T_{core}(w)\) — полная формальная трасса, читающая только проекцию \(\rho(w)\); - \(\mathfrak B\) — заранее объявленное множество допустимых extension-реестров; - \(b_0,b_1\in\mathfrak B\); - для фиксированной записи \(r_*\) выполнено \(b_0(r_*)=\ell_0\), \(b_1(r_*)=\ell_1\), \(\ell_0\ne\ell_1\); - \(T_{core}\) не читает \(b_0\) или \(b_1\). ### Лемма Для любого селектора \(s\), читающего только \(T_{core}(w)\): \[ \exists b\in\{b_0,b_1\}: s(T_{core}(w))\ne b(r_*). \] ### Доказательство Селектор получает одну и ту же трассу для обоих допустимых реестров и возвращает одну строку \(\ell\). Но \(\ell_0\ne\ell_1\), поэтому одна \(\ell\) не совпадает с обеими. \(\square\) Лемма не утверждает, что один реестр «истинен». Она устанавливает только невозможность воспроизвести две различающиеся строки непрочитанного реестра из одного и того же формального входа. ## 8. Машинные свидетели ### 8.1. Proof-object proof_formal.json содержит минимальную формальную систему копирования: FORMAL-AXIOM создаёт \(M(p)\), FORMAL-COPY возвращает \(M(p)\). Статус VALID-FORMAL означает только соответствие правилам MRB-0. proof_with_bridge.json добавляет \(B(b0)\), \(L_{b0}(p,q0)\) и BRIDGE-INTRO. Заключение \(A_{b0}(q0)\) принимается со списком bridge_dependencies = [b0]. proof_autonomous_attempt.json пытается получить \(A(q0)\) правилом FORMAL-COPY. Проверка отклоняет его кодом FORMAL_RULE_OUTPUT_KIND. Эти три файла проверяют саму границу типов. Они не являются ракетой, событием или целью. ### 8.2. Свежий extension-код witness_beyond.json содержит один и тот же core: - UTF-8-строку «p» с переводом строки; - атом p и аксиомную строку p; - корректный шаг копирования p; - один канонический SHA-256. Контракт заранее объявляет claim_id = q0 свежим: токен q0 отсутствует во всех строковых полях формального core. Он также заранее разрешает ровно два булевых значения q0. Два элемента закрытого \(K\) сохраняют \(\rho(k)=k.core\), но имеют false и true. Метапроверяющий \(V\) читает всю пару, подтверждает допустимость обоих значений и выдаёт BEYOND-RECORD. Формальная трасса \(T_{core}\) читает только core. Метапроверяющий \(V\neq T_{core}\). Статус означает различие двух разрешённых кодов при одинаковой проекции core, а не различие событий. Контроль witness_determined.json использует false в обоих элементах и получает RECORD-DETERMINED только относительно закрытой пары. ## 9. Ракета: максимальная уступка как аудит типов Запишем последовательность audit-кодов: \[ \mathsf M(\ulcorner\text{расчёт завершён}\urcorner), \] \[ \mathsf A_b(\ulcorner\text{ракета летит}\urcorner), \] \[ \mathsf V_{b,g} (\ulcorner\text{полёт}\urcorner, \ulcorner\text{имеет смысл}\urcorner). \] MRB-0 не присваивает этим строкам отношения к объекту или событию. Он проверяет только их типы и зависимости. Даже при максимальной уступке — если в расширенном контракте принято второе суждение как \(A_b\) — его proof-object содержит \(b\). Третье суждение требует ещё и \(g\). Формальная запись расчёта не создаёт пустой proof-object для \(A\), а \(A\)-суждение не создаёт пустой proof-object для \(V\). Противоположная строка «не имеет смысла» также требует целевого контракта. Поэтому MRB-0 не выбирает ни «смысл есть», ни «смысла нет». Горизонт «100/200/300 лет» является ещё одним payload до объявления правила \(G\). Увеличение числовой строки не добавляет goal_dependency. ## 10. Что доказано полностью Доказано: \[ \neg AME_{\mathcal C}. \] Это полный инвариант происхождения принятого proof-object в точном контракте MRB-0. Для переноса на иной корпус требуется проверенный контракт \(\tau\); без него неограниченное применение не заявляется. Точная строка: > В MRB-0 не существует принятого proof-object, который из одних суждений типа M получает суждение типа A с пустым множеством bridge_dependencies. Также доказана условная лемма: > Если два заранее допустимых extension-реестра различаются, формальная трасса, не читающая их, не идентифицирует оба реестра. Для всего параметрического класса \(\mathfrak C_{MRB}\) доказано: произвольные внутренние правила \(M^k\to M\) не меняют bridge-разрез; полная \(M\)-проекция сохраняется, а все \(A\)-шаги исчезают. Исполняемый аудит конкретного MRB-0 воспроизводит конечный случай. Не доказаны и не отрицаются: - существование или несуществование названного строками; - истинность или ложность прикладного payload; - невозможность вычисления, инженерии, управления или полёта; - наличие или отсутствие цели; - историческое происхождение математики; - глобальная фраза «математика опровергнута». Глобальная фраза получает UNBOUNDED-STANDALONE. Это не уступка математике. Это запрет данному тексту присвоить себе именно тот неучтённый переход, который MRB-0 запрещает приписывать собственным принятым proof-object без зарегистрированной зависимости. ## 11. Финал > Формальный вывод принят. > Его заключение имеет тип M. > Прикладной тип A появляется только в правиле, записывающем мостовую зависимость. > Целевой тип V появляется только с отдельной goal_dependency. > > Поэтому в MRB-0 автономный экспорт \(\Gamma_M;\varnothing\vdash A(q)\) полностью отвергнут. > > Доказательство завершило формальную запись. > Переход к прикладной строке в нём отсутствует. Авторская кода: > Человек выучил звук > и стал этим звуком, > пытающимся улететь на Марс. > > Статус: LITERARY-CODA. Не теорема.