Текущий контекст строит поле ближайших ходов; фиксированный контракт Q* выделяет допустимые, а локальный рейтинг qt упорядочивает их.
The current context constructs a field of near transitions; a fixed contract Q* identifies admissible ones, while the local rank qt orders them.
Она возникает как кандидат внутри текущего контекста: памяти прошлых срезов, шума, люфта, границы допустимости и критерия качества. Контекст создаёт поле ближайших целей; отдельный селектор выбирает ход из этого поля.
It arises as a candidate within the current context: memory of past slices, noise, slack, an admissibility boundary, and a quality criterion. Context creates the connectedness; a separate selector chooses a move from that field.
Здесь контекст не равен архиву. Это активная память: прошлые срезы удерживаются не целиком, а через фильтры, шум и границу того, что сейчас вообще можно считать допустимым ходом.
Here context is not an archive. It is active memory: past slices are retained not in full, but through filters, noise, and the boundary of what can count as an admissible move now.
В динамической семантике контекст рассматривается как информационное состояние, которое обновляется действием или высказыванием. Это поддерживает чтение контекста как состояния перехода, а не как неподвижного фона.
In dynamic semantics, context is treated as an information state updated by an action or utterance. This supports reading context as a state of transition rather than a static backdrop.
В теории жизнеспособности сначала задаётся множество состояний и траекторий, которым разрешено не покидать границу. Это даёт точный внешний язык для «ближайших допустимых ходов».
In viability theory one first specifies states and trajectories allowed to remain within a boundary. This provides a precise external language for “near admissible moves.”
В геометрии поле связывает каждую точку с локальными данными. В теории жизнеспособности эти данные могут быть множеством допустимых направлений. Наше поле ближайших целей использует ту же форму: каждой контекстной позиции оно ставит в соответствие множество ближайших допустимых кандидатов.
In geometry, a field associates each point with local data. In viability theory, those data can be a set of admissible directions. Our connectedness uses the same form: it associates each contextual position with a set of nearest admissible candidates.
Векторное поле является сечением касательного расслоения: каждой точке многообразия ставится в соответствие касательный вектор.
A vector field is a section of the tangent bundle: it associates each point of a manifold with a tangent vector.
Теория жизнеспособности работает с многозначными отображениями и дифференциальными включениями для состояния с несколькими допустимыми продолжениями.
Viability theory works with set-valued maps and differential inclusions for a state with several admissible continuations.
Aubin and Frankowska, Set-Valued Analysis and Viability Theory ↗
В рабочей модели вводим контекстную позицию как пятёрку. Это кандидатная нотация модели.
In the working model we introduce a contextual position as a five-tuple. This is candidate notation for the model.
Gᵣ(Xₜ) задаёт множество ближайших кандидатов. Фиксированный контракт Q* вместе с объявленным состоянием свидетельств Ht выделяет множество At, а qt только упорядочивает уже допустимые варианты.
Gᵣ(Xₜ) specifies the set of nearest candidates. The fixed contract Q* together with the declared evidence state Ht determines At, while qt only orders already admissible options.
Блуждание зондирует область по нескольким кандидатным линиям и удерживает различающую границу в поле.
Wandering probes an area through several candidate lines and keeps the distinguishing boundary in the field.
Нужно отображение α от внешней модели к типам и отношениям рабочей модели. Оно сохраняет допустимость, границу и различимость кандидатов.
A map α is needed from an external model into working-model types and relations. It preserves admissibility, boundary, and distinguishability of candidates.
Идея конкретного и абстрактного носителя с явным отношением между ними даёт дисциплину: перечислить, что перенос сохраняет, вместо того чтобы объявлять перенос эквивалентностью.
The idea of concrete and abstract carriers with an explicit relation supplies discipline: list what a transport preserves instead of declaring it an equivalence.
Встроенный Lean-каркас задаёт типы контекста, действия и шума, а также поле и селектор. Его роль в текущей карте - подготовить проверяемый формальный носитель.
The embedded Lean frame defines types for context, action, and noise, together with a field and selector. Its role in the current map is to prepare a checkable formal carrier.
ВСТРОЕННЫЙ LEAN-КОНТУР ↓EMBEDDED LEAN FRAME ↓
Lean Language Reference ↗ — внешний язык и правила проверки.— external language and proof-checking rules.
Mathlib Set API ↗ — внешняя документация для импортируемого носителя множеств.— external documentation for the imported set carrier.
Если поле построено, следующая цель ещё не доказана. Она появляется только после явного селектора.
Once a field is built, the next goal is not yet proved. It appears only after an explicit selector.
Следующий шаг: задать один конечный пример — три позиции, конечное множество действий, явный шум, границу K, фиксированный контракт Q*, проекцию η и локальный рейтинг q. Затем вручную выписать Gᵣ(X), A и показать, что переход α сохраняет кандидатов.
The next step: specify one finite example — three positions, a finite action set, explicit noise, a boundary K, a fixed contract Q*, a projection η, and a local rank q. Then list Gᵣ(X), A, and show that α preserves candidates.
Если этот пример пройдёт без скрытого выбора и без потери различимости, появится первый проверяемый мост рабочей модели между блужданием, полем целей и выбором.
If this example passes without hidden selection or loss of distinguishability, it yields the first testable working-model bridge between wandering, the goal field, and selection.
Сейчас мы думаем не о симплексах вообще, а о симплициальном носителе первичного различения. Нулевой симплекс отмечает саму границу.
We are not thinking about simplices in general, but about a simplicial carrier of primary distinction. The zero-simplex marks the boundary itself.
Какой носитель делает это различение минимальным и сохраняет его при переходе к следующему симплициальному уровню? Частичный рабочий ответ R-01 строит интерфейсную границу с двумя ролями.
Which carrier makes this distinction minimal and preserves it when moving to the next simplicial level? Partial working response R-01 constructs an interface boundary with two roles.
Следующая рабочая аксиома различает не просто линию, а интерфейсную границу. Она минимально несёт две роли.
The next working axiom distinguishes not just a line, but an interface boundary. It minimally carries two roles.
R-01 / частичный рабочий ответ на Q-01 ↑
R-01 / partial working response to Q-01 ↑
Двухсторонность различает локальное чтение носителя и его глобальную организацию. Теорема Жордана-Брауэра даёт две компоненты дополнения для вложенной сферы.
Two-sidedness distinguishes a local reading of a carrier from its global organization. The Jordan-Brouwer theorem gives two complementary components for an embedded sphere.
One-sided and two-sided surfaces, EoM ↗
Jordan-Brouwer notes ↗
Топология узлов даёт язык вложенной окружности; теория tangle даёт язык правильно вложенного одномерного многообразия с концами.
Knot theory gives a language for an embedded circle; tangle theory gives a language for a properly embedded one-dimensional manifold with endpoints.
Первый носитель линии различения будет замкнутой окружностью S¹ или разомкнутой дугой/tangle? Для выбора нужно назвать пространство M, правило концов и отображение в следующий симплициальный уровень.
Will the first carrier of the distinction line be a closed circle S¹ or an open arc/tangle? The choice needs a space M, an endpoint rule, and a map to the next simplicial level.
Берём один кубит как конечный внешний носитель. Его редуцированное состояние служит контекстом, а канал фазовой декогеренции выделяет поле устойчивых различимых записей.
Take one qubit as a finite external carrier. Its reduced state serves as context, while a phase-decoherence channel identifies a field of stable distinguishable records.
Доказательство. Равенство Dλ(ρ) = ρ даёт (1 − λ)b = 0. Из |λ| < 1 следует b = 0, поэтому ρ ∈ GΔ. Каждая диагональная ρ(p) сохраняется каналом, следовательно Fix(Dλ) = GΔ.
Proof. The equality Dλ(ρ) = ρ gives (1 − λ)b = 0. Since |λ| < 1, b = 0, hence ρ ∈ GΔ. Each diagonal ρ(p) is preserved by the channel, so Fix(Dλ) = GΔ.
Доказательство. На отрезке [0, 1] функция −(p − q)² достигает единственного максимума 0 в p = q. Поэтому πQq(GΔ) = ρ(q). По A-04 Dλ(ρ(q)) = ρ(q).
Proof. On [0, 1], the function −(p − q)² reaches its unique maximum 0 at p = q. Thus πQq(GΔ) = ρ(q). By A-04 Dλ(ρ(q)) = ρ(q).
Внешняя опора. В теории декогеренции взаимодействие системы со средой подавляет интерференцию между pointer-состояниями и выделяет устойчивые записи: Zurek; формальный обзор каналов и моделей: Schlosshauer.
External support. In decoherence theory, system-environment interaction suppresses interference between pointer states and identifies stable records: Zurek; for a formal overview of channels and models: Schlosshauer.
Построить правило F : Cₜ ↦ qₜ ∈ [0, 1], затем доказать, что gₜ = ρ(F(Cₜ)) остаётся в GΔ при каждом шаге декогеренции.
Construct a rule F : Cₜ ↦ qₜ ∈ [0, 1], then prove that gₜ = ρ(F(Cₜ)) remains in GΔ at every decoherence step.
Маршрут переводит контекстную позицию в параметр устойчивого состояния и проверяет сохранение выбранной записи заданным каналом.
The route translates a contextual position into a stable-state parameter and checks preservation of the selected record by a specified channel.
Зафиксировать систему S, пространство состояний и начальное состояние ρₜ как читаемый физический носитель контекста.
Fix a system S, its state space, and an initial state ρₜ as a readable physical carrier of context.
Задать среду E и карту взаимодействия: гамильтонианную модель или квантовый канал Dλ.
Specify an environment E and an interaction map: a Hamiltonian model or a quantum channel Dλ.
Выбрать базис устойчивых записей P, шаг времени Δt и масштаб огрубления ε, на котором запись читается как различимая.
Choose a stable-record basis P, a time step Δt, and a coarse-graining scale ε at which the record is read as distinguishable.
Построить F : Cₜ ↦ qₜ и проверить, что выбранное состояние ρ(qₜ) сохраняется картой Dλ.
Construct F : Cₜ ↦ qₜ and check that the selected state ρ(qₜ) is preserved by Dλ.
Zurek ↗ — внешний факт: декогеренция и устойчивые pointer-записи.— external fact: decoherence and stable pointer records.
Schlosshauer ↗ — внешний факт: язык каналов и моделей декогеренции.— external fact: the language of channels and decoherence models.
Оформить одну карточку спецификации системы S с полями E, взаимодействие, P, Δt, ε и входами для F.
Write one specification card for system S with fields E, interaction, P, Δt, ε, and inputs for F.
Карточка задаёт один воспроизводимый носитель для перехода от контекста к устойчивой записи.
This card specifies one reproducible carrier for the transition from context to a stable record.
Состояние живёт в Hₛ = ℂ²; базис P задаёт два различимых исхода записи.
The state lives in Hₛ = ℂ²; the basis P specifies two distinguishable record outcomes.
Среда задаётся как источник фазового шума; её действие на запись представлено каналом Dλ.
The environment is specified as a source of phase noise; its action on the record is represented by Dλ.
Δt задаёт шаг эволюции, а ε задаёт разрешение, при котором диагональная запись читается как устойчивая.
Δt specifies an evolution step, while ε specifies the resolution at which a diagonal record is read as stable.
F принимает Cₜ и выдаёт qₜ ∈ [0, 1]; запись gₜ = ρ(qₜ) проходит тест Dλ(gₜ) = gₜ.
F takes Cₜ and returns qₜ ∈ [0, 1]; the record gₜ = ρ(qₜ) passes the test Dλ(gₜ) = gₜ.
Zurek ↗ — внешний факт: декогеренция выделяет устойчивые записи.— external fact: decoherence identifies stable records.
Schlosshauer ↗ — внешний факт: язык каналов и моделей декогеренции.— external fact: the language of channels and decoherence models.
Задать входные компоненты Cₜ, от которых F вычисляет qₜ.
Specify the components of Cₜ from which F computes qₜ.
Формульный слой теперь использует только символы и латинские идентификаторы. Русское и английское чтения остаются в парных текстовых узлах рядом с записью.
The formula layer now uses only symbols and Latin identifiers. Russian and English readings remain in paired prose nodes beside the notation.
Для объявленного домена D рост задаётся связанным переходом g_D между двумя состояниями корпуса. Инвариант I_D переносится явно заданным транспортом τ_g.
For a declared domain D, growth is given by a connected transition g_D between two corpus states. The invariant I_D is carried by an explicitly specified transport τ_g.
Это кандидатное правило рабочего корпуса: новая часть принимается как рост, когда её связь с доменом и перенос инварианта предъявлены вместе.
This is a candidate rule for the working corpus: a new part counts as growth when its domain connection and invariant transport are exhibited together.
К границе утверждения B-09 ↓Claim boundary B-09 ↓Для ответа нужно выбрать домен, интерфейс, наблюдаемую величину и правило проверки переноса.
Answering it requires choosing the domain, interface, observable, and a transport-check rule.
Статус и условия в B-09 ↓Status and conditions in B-09 ↓Эти источники дают проверяемые механизмы для отдельных частей правила g_D / τ_g: совместимость отображений, инвариантность при деформации, продолжение динамического индекса и устойчивые физические состояния.
These sources provide checkable mechanisms for separate parts of the g_D / τ_g rule: compatibility of maps, invariance under deformation, continuation of a dynamical index, and stable physical states.
Компоненты переноса согласуются со всеми морфизмами. Это внешний язык для требования, чтобы τ_g уважал структуру перехода.
Transport components commute with every morphism. This gives external language for requiring τ_g to respect transition structure.
↗ Stacks Project · external terminologyСтандартный топологический маршрут связывает гомотопическую инвариантность, симплициальную и сингулярную гомологию. Он задаёт внешний контроль для выбора носителя.
The standard topological route connects homotopy invariance with simplicial and singular homology. It provides external control for choosing a carrier.
↗ Hatcher, Algebraic Topology · external factДля изолированного инвариантного множества индекс Конли имеет свойство continuation. Это внешний пример того, как инвариант получает смысл вдоль контролируемого семейства.
For an isolated invariant set, the Conley index has a continuation property. This is an external example of an invariant acquiring meaning along a controlled family.
↗ Floer, continuation of the Conley index · external factВ модели открытой квантовой системы взаимодействие со средой выделяет устойчивые pointer states. Это физическая опора для отдельного теста носителя, не доказательство правила g_D / τ_g.
In an open quantum system, interaction with an environment selects stable pointer states. This is physical support for a separate carrier test, not a proof of the g_D / τ_g rule.
↗ Zurek, decoherence and einselection · physical analogyПубличное обозначение: «черновик · исследовательская запись · рабочий журнал · кандидат C-01». Каждый слой сообщает читателю, как с этим носителем можно работать.
The public designation is “draft · research note · working journal · candidate C-01”. Each layer tells a reader how this carrier may be used.
«Связность» — имя кандидата и имя рабочего поля C-01.
“Connectedness” is the name of the candidate and the working field of C-01.
К границе утверждения B-11 ↓Claim boundary B-11 ↓Рабочая модель «Связность» задаёт поле продолжений, интерфейс и перенос инварианта. Квантовый случай возникает после явного задания двух подсистем, их совместного состояния и теста разделимости.
The working model “Connectedness” specifies a field of continuations, an interface, and invariant transport. A quantum case arises after two subsystems, their joint state, and a separability test are explicitly specified.
Здесь специальное правило Fent проверяет принадлежность ρAB классу разделимых состояний либо применяет явный entanglement witness.
Here the special rule Fent tests whether ρAB belongs to the separable-state class or applies an explicit entanglement witness.
↗ Horodecki et al. / external definition · ↗ IBM Quantum Learning / terminology · ↗ Zurek / physical context
Паспорт, журнал, утверждения, границы и реестр источников записаны непосредственно в HTML. После открытия страницы карта строит из них 2D-граф: объект остаётся статичной точкой, а каждая логическая стрелка ведёт к развороту связанного фрагмента.
The passport, journal, statements, boundaries, and source ledger are written directly into the HTML. After opening, the map builds a 2D graph from them: an object remains a static point, while each logical arrow leads to the unfolding of its linked fragment.
К границе утверждения B-13 ↓Claim boundary B-13 ↓Рабочее отношение связности получает физический тест в явно заданной двухчастной системе H = HA ⊗ HB. Мы задаём состояние ρ, взаимодействие, устойчивый базис, масштаб и правило F, затем сопоставляем сепарабельный и неразделимый случаи.
The working relation of connectedness receives a physical test in an explicitly specified bipartite system H = HA ⊗ HB. We specify the state ρ, interaction, stable basis, scale, and rule F, then compare separable and nonseparable cases.
Werner ↗ — внешняя фактологическая опора для различения сепарабельных и неразделимых состояний. Schrödinger ↗ — терминология и исторический контекст составных и разделённых систем.
Werner ↗ is an external factual support for the distinction between separable and nonseparable states. Schrödinger ↗ supplies terminology and historical context for composite and separated systems.
Следующий ход: задать минимальную двухуровневую систему и проверить различение на паре состояний.
Next move: specify a minimal two-level system and test the distinction on a pair of states.
Для каждого нового материального узла фиксируются собственный якорь, прямой переход с карты, запись в источниках и дельта паспорта, когда меняется текущий статус корпуса.
For each new material node, the reader records its own anchor, a direct map transition, a source-ledger entry, and a passport delta whenever the current corpus status changes.
Кандидат Lean отделяет физический интерфейс, предикаты связности, сепарабельности и неразделимости, а также проверяемый свидетель различения. Читательский снимок кода встроен ниже в эту страницу.
The Lean candidate separates the physical interface, predicates for connectedness, separability, and nonseparability, and a testable witness of distinction. A reader-facing code snapshot is embedded below in this page.
Карта остаётся навигационным носителем: каждый её переход ведёт к содержательному блоку по устойчивому внутреннему адресу, а не к промежуточной служебной подписи.
The map remains a navigation carrier: each transition leads to the material block through a stable internal address rather than to an intermediate service label.
Квантовый компьютер готовит регистр кубитов, применяет квантовые операции, согласует схему с ограничениями конкретного QPU и переводит измерение в классический результат. В рабочей карте это становится контекстом CtQ = (схема, target, калибровка, время, FQ).
A quantum computer prepares a register of qubits, applies quantum operations, matches a circuit to the constraints of a particular QPU, and transfers measurement into a classical result. In the working map this becomes a context CtQ = (circuit, target, calibration, time, FQ).
Транспиляция переписывает абстрактную схему так, чтобы она соблюдала набор операций, связность и временные ограничения выбранного квантового процессора.
Transpilation rewrites an abstract circuit so that it obeys the instruction set, connectivity, and timing constraints of a selected quantum processor.
IBM Quantum: Introduction to transpilation ↗ — внешний факт.— external fact.
Измерение кубита сохраняет результат в классическом регистре; это ясный физический интерфейс между квантовым состоянием и читаемым носителем.
Measuring a qubit stores the result in a classical register; this is a clear physical interface between a quantum state and a readable carrier.
IBM Quantum: Construct circuits ↗ — внешний факт.— external fact.
FQ собирает явные критерии выбора: совместимость с target, оценку ошибки, глубину схемы, число вентилей и время выполнения. Селектор выбирает один исполнимый кандидат из поля.
FQ collects explicit selection criteria: target compatibility, error estimate, circuit depth, gate count, and execution time. The selector chooses one executable candidate from the field.
Квантовый регистр может нести базисное кодирование k-симплексов фиксированного классического комплекса: Eₖ(σₖ) = |σₖ⟩. В квантовом алгоритме для топологического анализа симплексы комплекса представляются квантовыми состояниями. ↗ S-26 / внешний факт · К границе утверждения B-15 ↓
A quantum register can carry a basis encoding of k-simplices of a fixed classical complex: Eₖ(σₖ) = |σₖ⟩. In a quantum algorithm for topological analysis, simplices of the complex are represented as quantum states. ↗ S-26 / external fact · Claim boundary B-15 ↓
Eₖ : σₖ ↦ |σₖ⟩ · ∂ₖ : Cₖ → Cₖ₋₁ · μ : Register → Outcome
Рабочая карта разделяет классический комплекс K, кодирование Eₖ и измеряемое чтение μ. Формальная граница ∂ₖ остаётся оператором модели; её исполнимый носитель обозначаем C∂.
The working map separates the classical complex K, the encoding Eₖ, and measured readout μ. The formal boundary ∂ₖ remains a model operator; its executable carrier is denoted C∂.
Зафиксировать конечный комплекс K, явное Eₖ, схему C∂ и протокол μ; затем сравнить измеряемый результат с матрицей классической границы ∂ₖ.
Fix a finite complex K, an explicit Eₖ, a circuit C∂, and a protocol μ; then compare the measured result with the classical boundary matrix ∂ₖ.
Смежная динамическая линия строит квантовое блуждание, кодирующее комбинаторный лапласиан симплициального комплекса. ↗ S-27 / внешний факт
An adjacent dynamic line constructs a quantum walk encoding the combinatorial Laplacian of a simplicial complex. ↗ S-27 / external fact
universe u v w
structure QuantumSimplicialCarrier (Simplex : Type u) (Register : Type v) (Outcome : Type w) where
encode : Simplex → Register
boundary : Simplex → List Simplex
measure : Register → Outcome
valid : Simplex → PropЭтот фрагмент задаёт типы и стрелки кандидата; он соответствует встроенному формальному приложению. К Lean-кандидату ↓
This fragment fixes the candidate types and arrows; it matches the embedded formal appendix. Lean candidate ↓
Терминологическая соседняя ветвь: в spin-foam исследованиях 4-симплекс служит строительным блоком квантово-геометрической амплитуды. Здесь это отмечено как аналогия языка. ↗ S-28 / аналогия
Terminological adjacent line: in spin-foam research a 4-simplex serves as a building block for a quantum-geometric amplitude. This is recorded here as an analogy of language. ↗ S-28 / analogy
Текущая модель уже задаёт позиции C, допустимые переходы C → C′ и выбор следующего хода π. Это образует граф переходов, который можно предъявить квантовому носителю. К границе утверждения B-16 ↓
The current model already specifies positions C, admissible transitions C → C′, and a next-step selector π. This forms a transition graph that can be presented to a quantum carrier. Claim boundary B-16 ↓
Cᵢ ↦ |Cᵢ⟩ · Cᵢ → Cⱼ ↦ Uᵢⱼ · μ(|ψ⟩) ↦ classical record
Квантовый интерфейс сохраняет различение между состоянием, переходом и чтением: узел кодируется как базисное состояние, переход — как компонент оператора U, а измерение μ возвращает классическую запись.
The quantum interface preserves the distinction between state, transition, and readout: a node is encoded as a basis state, a transition as a component of an operator U, and measurement μ returns a classical record.
Выбрать конечный трёхузловой подграф текущего поля, задать базис |C₀⟩, |C₁⟩, |C₂⟩, записать кандидата U и протокол μ, затем сравнить допустимые классические рёбра с ненулевыми амплитудами перехода.
Choose a finite three-node subgraph of the current field, fix the basis |C₀⟩, |C₁⟩, |C₂⟩, write a candidate U and a protocol μ, then compare admissible classical edges with nonzero transition amplitudes.
Внешняя работа строит квантовое блуждание, кодирующее комбинаторный лапласиан симплициального комплекса. Она поддерживает форму перехода, но не подменяет наш критерий F. ↗ S-27 / внешний факт
External work constructs a quantum walk encoding the combinatorial Laplacian of a simplicial complex. It supports the transition form, but does not substitute for our criterion F. ↗ S-27 / external fact
structure QuantumWalkInterface (State : Type u) (Register : Type v) (Outcome : Type w) where
encode : State → Register
step : Register → Register
measure : Register → Outcome
admissible : State → State → PropКод фиксирует типы и стрелки интерфейса; проверка свойств U относится к T-QW-01. К формальному приложению ↓
The code fixes the interface types and arrows; checking the properties of U belongs to T-QW-01. Formal appendix ↓
Публичная запись фиксирует доступный извне снимок рабочего ридера и даёт ему устойчивый идентификатор для ссылки и цитирования.
The public record fixes an externally accessible snapshot of the working reader and gives it a stable identifier for linking and citation.
P-01 ↗ Zenodo DOI: 10.5281/zenodo.21430887 — публичная запись и якорь происхождения.— public record and provenance anchor.
Для текущей карты фиксируем минимальный носитель различения: два ориентированных 1-симплекса с общей центральной вершиной. Он переводит роли ЭТО → граница → НЕ-ЭТО в видимую геометрию.
For the current map, we fix a minimal carrier of distinction: two oriented 1-simplices with one shared central vertex. It translates the roles THIS → boundary → NOT-THIS into visible geometry.
Γ¹∂ = [vin, v∂] + [v∂, vout]
Γ¹∂ = [vin, v∂] + [v∂, vout]
Отображение ι задаётся на вершинах как ι(vin) = 0, ι(v∂) = 1, ι(vout) = 2; поэтому ι(Γ¹∂) = [0,1] + [1,2] ⊂ ∂Δ².
The map ι is fixed on vertices by ι(vin) = 0, ι(v∂) = 1, ι(vout) = 2; hence ι(Γ¹∂) = [0,1] + [1,2] ⊂ ∂Δ².
Ориентированный двухрёберный путь задаёт рабочий геометрический носитель различения и явный переход в границу 2-симплекса. См. границу B-18 ↓
The oriented two-edge path defines a working geometric carrier of distinction and an explicit transition into the boundary of a 2-simplex. See claim boundary B-18 ↓
Для пути Γ¹∂ фиксирован отдельный малый носитель чтения: внутри → граница → снаружи.
For the path Γ¹∂, a separate small readout carrier is fixed: inside → boundary → outside.
Носитель разводит кодирование, стабилизацию и чтение. Его два ориентированных перехода идут от «внутри» к «границе» и от «границы» к «снаружи».
The carrier separates encoding, stabilization, and readout. Its two oriented transitions go from inside to boundary and from boundary to outside.
Формальный каркас кандидата вынесен в ↓ снимок Lean-носителя, чтобы рабочая линия оставалась читаемой.
The candidate's formal skeleton is kept in the ↓ Lean-carrier snapshot, so the working line remains readable.
Внешние опоры: ↗ IBM Quantum Learning, внешний факт для базисного измерения; ↗ Zurek, терминология для языка устойчивого чтения.
External support: ↗ IBM Quantum Learning, external fact for basis measurement; ↗ Zurek, terminology for the language of stable readout.
↓ A-18 / кандидатный формальный мост · ↓ снимок Lean-носителя · ↓ B-19 / граница утверждения
↓ A-18 / candidate formal bridge · ↓ Lean-carrier snapshot · ↓ B-19 / claim boundary
Код 00, 01, 10 несёт роли «внутри», «граница» и «снаружи»; явные предпосылки стабилизации и измерения выводят возврат каждой кодовой роли, а предпосылка refinement выводит реализацию двух ориентированных рёбер Γ¹∂.
The code 00, 01, 10 carries the roles inside, boundary, outside; explicit stabilization and measurement assumptions yield recovery of every coded role, while a refinement assumption yields realization of the two oriented edges of Γ¹∂.
Берём один конечный контекст C₀ с носителем Γ¹∂. Его поле ближайших ходов состоит из двух ориентированных рёбер: Gᵣ(C₀) = {[vin, v∂], [v∂, vout]}. Ролевая метка rΓ задаёт внутри, границу и снаружи на трёх вершинах.
Take one finite context C₀ with carrier Γ¹∂. Its field of nearby moves consists of two oriented edges: Gᵣ(C₀) = {[vin, v∂], [v∂, vout]}. The role label rΓ assigns inside, boundary, and outside to the three vertices.
Задаём α(vin) = 0, α(v∂) = 1, α(vout) = 2 и читаем 0, 1, 2 соответственно как inside, boundary, outside. Тогда оба ребра переходят в [0,1] и [1,2], а метки трёх ролей сохраняются буквально.
Set α(vin) = 0, α(v∂) = 1, α(vout) = 2 and read 0, 1, 2 respectively as inside, boundary, outside. Then the two edges map to [0,1] and [1,2], while the labels of all three roles are preserved literally.
Для одного именованного конечного носителя выбор сделан: M = Γ¹∂, правило концов задаётся двумя ориентированными рёбрами, а переход к следующему уровню задаёт α = ι.
For one named finite carrier, the choice is fixed: M = Γ¹∂, the endpoint rule is given by two oriented edges, and the transition to the next level is α = ι.
Равенство rΔ ∘ α = rΓ связывает исходные вершины, два ориентированных ребра и их образы на границе Δ². К границе B-20 ↓
The equality rΔ ∘ α = rΓ links the source vertices, the two oriented edges, and their images on the boundary of Δ². To boundary B-20 ↓
J-22 / источники: новых внешних опор нет; это явная проверка внутри уже зафиксированного авторского конечного носителя.J-22 / sources: no new external support; this is an explicit check inside the already fixed authorial finite carrier.
Во внешней квантовой модели конечный потенциальный барьер B(U₀, L) может дать ненулевую переданную компоненту ψout для состояния ψin. Для нашей рабочей карты это не снятие границы, а различённый переход: внутри → конечная граница → внешний носитель.
In the external quantum model, a finite potential barrier B(U₀, L) can yield a nonzero transmitted component ψout for a state ψin. For our working map, this is not removal of the boundary but a distinguished transition: inside → finite boundary → external carrier.
В поле ближайших ходов Gτ(C) вводится именованный кандидат τtun: параметры U₀, L, E и порог τ должны быть явными. Проверка шага состоит в вычислении или измерении T и сопоставлении его с заранее заданным порогом.
The field of nearby moves Gτ(C) receives a named candidate τtun: the parameters U₀, L, E, and threshold τ must be explicit. The step is checked by calculating or measuring T and comparing it with the predeclared threshold.
При заданных U₀, L, E и τ выражение T(U₀, L, E) ≥ τ задаёт наблюдаемый критерий перехода от внутреннего состояния к внешнему носителю. К границе B-21 ↓
For specified U₀, L, E, and τ, the expression T(U₀, L, E) ≥ τ defines an observable criterion for transition from an internal state to an external carrier. To boundary B-21 ↓
J-23 / внешняя опора: квантовое туннелирование через конечный потенциальный барьер — ↓ S-31.J-23 / external support: quantum tunneling through a finite potential barrier — ↓ S-31.
Рабочая машина получает три явно различённые роли: Q* задаёт постоянное правило допустимости, Et хранит накопленный след, а qt упорядочивает только уже допустимые кандидаты. Проекция η извлекает из следа Ht — объявленную часть свидетельств, которую контракт имеет право читать.
The working machine receives three explicitly distinct roles: Q* gives a stable admissibility rule, Et stores the accumulated trace, and qt orders only already admissible candidates. The projection η extracts Ht from the trace — the declared evidence portion that the contract may read.
При заданных Xt и Ht правило Q* формирует At; рейтинг qt действует только после этого формирования. К границе B-22 ↓
For specified Xt and Ht, the rule Q* forms At; the rank qt acts only after that formation. To boundary B-22 ↓
Статус: OPEN QUESTION. Нужен конечный перечень полей η, их типы и правило аудита каждого поля.
Status: OPEN QUESTION. A finite list of η fields, their types, and an audit rule for each field are required.
J-24 / внешние опоры: ↓ S-32 даёт терминологию происхождения и прослеживаемости; ↓ S-33 даёт терминологическое различение постоянного параметра и изменяемого состояния. Они не подтверждают Q*, η или нашу кандидатную машину.J-24 / external supports: ↓ S-32 provides terminology for provenance and traceability; ↓ S-33 provides terminology for distinguishing a constant parameter and a changing state. They do not validate Q*, η, or our candidate machine.
Для трёх ролей фиксируется внешний математический каркас: кодирование создаёт состояние, канал Φ переносит его, а измерение возвращает конечный классический исход. Это даёт мосту форму, в которой каждое звено можно определить и проверить отдельно.
For the three roles, an external mathematical frame is fixed: encoding creates a state, the channel Φ transports it, and measurement returns a finite classical outcome. This gives the bridge a form in which every link can be defined and checked separately.
Для трёх исходов измерение задаётся эффектами Pin, P∂, Pout с суммой I; вероятность исхода получается из следа Prρ. Канал Φ должен быть задан как линейное преобразование матриц плотности.
For three outcomes, measurement is specified by effects Pin, P∂, Pout summing to I; the outcome probability is obtained from the trace Prρ. The channel Φ must be specified as a linear transformation of density matrices.
Для каждой роли r фиксируется целевое равенство чтения после канала. Оно связывает внутренний код, внешний носитель и конечный классический исход в одном проверяемом утверждении.
For every role r, a target readout equality after the channel is fixed. It connects the internal code, the external carrier, and the finite classical outcome in one checkable statement.
↓ Q-05 / выбор явного канала · ↓ B-23 / граница утверждения
↓ Q-05 / choosing an explicit channel · ↓ B-23 / claim boundary
Статус: PARTIAL ANSWER AVAILABLE. Конечная карта декогеренции выбрана для одного двухкубитного кодирования в R-04. Для закрытия вопроса остаются формальное доказательство Target(r) и перенос на иной носитель.
Status: PARTIAL ANSWER AVAILABLE. A finite decoherence map is chosen for one two-qubit encoding in R-04. Closing the question still requires a formal proof of Target(r) and transport to another carrier.
Внешние опоры: ↗ IBM Quantum Learning, внешний факт для конечного измерения через эффекты и след; ↗ IBM Quantum Learning, внешний факт для канала Φ; ↗ Quantum Computing in Lean, терминология для проверяемого носителя конечных состояний и измерений.
External support: ↗ IBM Quantum Learning, external fact for finite measurement through effects and traces; ↗ IBM Quantum Learning, external fact for the channel Φ; ↗ Quantum Computing in Lean, terminology for a checkable carrier of finite states and measurements.
Выбираем пространство C⁴ с вычислительным базисом 00, 01, 10, 11. Три роли занимают первые три базисных состояния; четвёртое остаётся резервной частью внешнего исхода.
Choose the space C⁴ with computational basis 00, 01, 10, 11. The three roles occupy the first three basis states; the fourth remains a reserve part of the external outcome.
Пусть Πb = |b⟩⟨b|. Выбираем полную декогеренцию в вычислительном базисе и трёхисходное измерение, где внешний исход объединяет 10 и 11.
Let Πb = |b⟩⟨b|. Choose complete dephasing in the computational basis and a three-outcome measurement in which the external outcome joins 10 and 11.
Поскольку Φ сохраняет диагональные проекторы Π00, Π01, Π10, проверяемая цель для всех трёх ролей принимает конечную форму через след эффекта и кодового состояния.
Because Φ preserves the diagonal projectors Π00, Π01, Π10, the checkable target for all three roles takes a finite form through the trace of an effect and a code state.
↓ R-04 / частичный ответ Q-05 · ↓ B-24 / граница утверждения
Кандидат Φ — полная декогеренция в вычислительном базисе. Она оставляет три выбранных кодовых проектора неизменными и переводит измерение в конечное сравнение следов.
The candidate Φ is complete dephasing in the computational basis. It leaves the three chosen code projectors unchanged and turns measurement into a finite comparison of traces.
J-26 / внешние опоры: ↗ S-34, IBM Quantum Learning, внешний факт задаёт измерение через эффекты и след; ↗ S-35, IBM Quantum Learning, внешний факт задаёт канал Φ. Новых внешних опор не добавлено.
J-26 / external support: ↗ S-34, IBM Quantum Learning, external fact specifies measurement through effects and traces; ↗ S-35, IBM Quantum Learning, external fact specifies the channel Φ. No new external supports are added.
Статус: OPEN QUESTION. Для продолжения нужны правило эквивалентности носителей, явное отображение αM и отдельная проверка сохранения трёх ролей после переноса.
Status: OPEN QUESTION. Continuation requires a carrier-equivalence rule, an explicit map αM, and a separate check that the three roles are preserved after transport.
↓ R-03 / partial answer · ↓ A-19 / finite check · ↓ B-20 / boundary
Для кода из J-26 каждой роли r сопоставлен один базисный индекс c(r): in ↦ 00, ∂ ↦ 01, out ↦ 10. Дальше маршрут разделяется на ортогональность, сохранение кодового проектора каналом и чтение эффектом.
For the code from J-26, each role r is assigned one basis index c(r): in ↦ 00, ∂ ↦ 01, out ↦ 10. The route then separates into orthogonality, channel preservation of the code projector, and readout by an effect.
Первое равенство задаёт ортогональность базисных проекторов. Второе фиксирует действие выбранной декогеренции на кодовом носителе. Третье читает роль через соответствующий эффект. Вместе они дают точную форму цели A-23.
The first equality specifies orthogonality of basis projectors. The second fixes the action of the chosen dephasing on the code carrier. The third reads the role through its corresponding effect. Together they give the exact form of target A-23.
↓ A-23 / цель чтения · ↓ Q-06 / формальный носитель · ↓ B-25 / граница утверждения
↓ A-23 / readout target · ↓ Q-06 / formal carrier · ↓ B-25 / claim boundary
Статус: OPEN QUESTION, есть частичный ответ. Кандидат Matrix выбран в R-05. Нужны явные определения матриц плотности, сопряжённого транспонирования, следа, проекторов, Φ и эффектов Ps, затем проверка трёх равенств без `sorry`.
Status: OPEN QUESTION, with a partial answer. The Matrix candidate is selected in R-05. Explicit definitions are needed for density matrices, conjugate transpose, trace, projectors, Φ, and the effects Ps, followed by a proof of the three equalities without `sorry`.
↓ A-24 / конечное ядро · ↓ R-05 / Matrix-кандидат · ↓ R-06 / локальный носитель · ↓ B-26 / граница импорта
↓ A-24 / finite kernel · ↓ R-05 / Matrix candidate · ↓ R-06 / local carrier · ↓ B-26 / import boundary
Внешняя опора: ↓ S-34 задаёт измерение через эффекты и след, ↓ S-35 задаёт язык канала. Три показанных равенства образуют кандидатное конечное доказательное ядро.
External support: ↓ S-34 supplies measurement through effects and traces, while ↓ S-35 supplies the language of a channel. The displayed three equalities form a candidate finite proof kernel.
Для одного двухкубитного примера фиксируем кандидатную основу: комплексная матрица размера 4 × 4 с конечным индексом. В неё естественно помещаются кодовые проекторы, канал Φ, эффекты измерения и след.
For the one two-qubit example, fix a candidate basis: a 4 × 4 complex matrix with a finite index. It naturally accommodates code projectors, the channel Φ, measurement effects, and trace.
Кандидат разделяет четыре слоя: матрица ρ, предикат состояния, канал Φ и измерение Ps. Это позволяет выписывать три равенства J-27 как отдельные цели в одном конечном типе.
The candidate separates four layers: matrix ρ, the state predicate, channel Φ, and measurement Ps. This allows the three equalities of J-27 to be stated as separate goals in one finite type.
↓ R-05 / частичный ответ Q-06 · ↓ B-26 / граница утверждения
Mathlib документирует матрицы с конечными индексами, сопряжённое транспонирование, след и положительную полуопределённость. Внешний проект Quantum Computing in Lean даёт терминологический и API-прецедент для состояний и измерений. Поэтому первый формальный файл должен сначала выразить минимальный матричный носитель, а обёртки измерения подключать после отдельной проверки совместимости.
Mathlib documents matrices with finite indices, conjugate transpose, trace, and positive semidefiniteness. The external Quantum Computing in Lean project provides terminology and an API precedent for states and measurements. Therefore the first formal file should express the minimal matrix carrier first, attaching measurement wrappers only after a separate compatibility check.
↓ Q-06 / открытый вопрос · ↓ A-25 / подпись · ↓ B-26 / граница
↓ Q-06 / open question · ↓ A-25 / signature · ↓ B-26 / boundary
Внешняя опора: ↓ S-37 для конечных матриц и сопряжённого транспонирования; ↓ S-38 для следа и положительной полуопределённости; ↓ S-36 как терминологический и API-прецедент.
External support: ↓ S-37 for finite matrices and conjugate transpose; ↓ S-38 for trace and positive semidefiniteness; ↓ S-36 as a terminology and API precedent.
В локальном носителе различены четыре кодовых слова q00, q01, q10, q11. Функции encode и decode фиксируют три роли, а структура StableReadoutBridge отделяет действие dephase от измерения measure.
In the local carrier, four codewords q00, q01, q10, q11 are distinguished. The functions encode and decode fix the three roles, while the StableReadoutBridge structure separates the action dephase from the measurement measure.
Снимок задаёт теоремы decode_encode, stable_readout и gamma_boundary_realized. Последняя собирает два перехода inside → boundary и boundary → outside из явно сформулированной предпосылки refinement.
The snapshot states the theorems decode_encode, stable_readout, and gamma_boundary_realized. The last one gathers the two transitions inside → boundary and boundary → outside from the explicitly stated refinement premise.
↓ R-06 / частичный ответ Q-06 · ↓ Q-07 / подъём · ↓ B-27 / граница утверждения
↓ R-06 / partial answer to Q-06 · ↓ Q-07 / lift · ↓ B-27 / claim boundary
Первый формальный слой использует существующие типы InterfaceRole, TwoQubitCodeword, encode, decode и StableReadoutBridge. Матрицы из J-28 образуют следующий слой: отдельный подъём, сохраняющий кодовые роли и цель чтения.
The first formal layer uses the existing types InterfaceRole, TwoQubitCodeword, encode, decode, and StableReadoutBridge. The matrices from J-28 form the next layer: a separate lift preserving the code roles and the readout target.
↓ Q-06 / открытый вопрос · ↓ Q-07 / следующий вопрос · ↓ B-27 / граница
↓ Q-06 / open question · ↓ Q-07 / next question · ↓ B-27 / boundary
Статус: OPEN QUESTION, частично формально проверен. Теорема lift_encode принята Lean для трёх ролей. Дальнейшая часть вопроса переносит проверку на матричные произведения проекторов и сохранение чтения.
Status: OPEN QUESTION, partially formally checked. The theorem lift_encode is accepted by Lean for the three roles. The remaining part of the question carries verification to matrix products of projectors and preservation of readout.
↓ A-26 / дискретный мост · ↓ R-07 / конструкция · ↓ R-08 / Lean-проверка · ↓ Q-08 / матричное ядро · ↓ B-29 / граница прогона
↓ A-26 / discrete bridge · ↓ R-07 / construction · ↓ R-08 / Lean check · ↓ Q-08 / matrix kernel · ↓ B-29 / run boundary
namespace TLFL
inductive InterfaceRole where
| inside | boundary | outside
inductive TwoQubitCodeword where
| q00 | q01 | q10 | q11
def encode : InterfaceRole → TwoQubitCodeword
| .inside => .q00
| .boundary => .q01
| .outside => .q10
structure StableReadoutBridge where
dephase : TwoQubitCodeword → TwoQubitCodeword
measure : TwoQubitCodeword → Option InterfaceRole
dephase_codeword : ∀ role, dephase (encode role) = encode role
measure_codeword : ∀ role, measure (encode role) = some role
theorem stable_readout (bridge : StableReadoutBridge)
(role : InterfaceRole) :
bridge.measure (bridge.dephase (encode role)) = some role := by
rw [bridge.dephase_codeword role, bridge.measure_codeword role]
end TLFLЛокальный носитель: содержательный снимок встроен выше как ↓ кодовое приложение. Это локальный проектный файл, а не внешняя опора; новых внешних источников для J-29 не добавлено.
Local carrier: the substantive snapshot is embedded above as a ↓ code appendix. It is a local project file, not external support; J-29 adds no external sources.
Для фиксированного вычислительного базиса выбираем каждому кодовому слову соответствующий диагональный проектор. Карта lift действует как фиксированный перевод дискретной метки в её матричный носитель.
For the fixed computational basis, assign each codeword its corresponding diagonal projector. The lift map acts as a fixed translation of a discrete label into its matrix carrier.
На трёх ролях применяется одна и та же таблица: lift(encode(in)) = Π₀₀, lift(encode(∂)) = Π₀₁, lift(encode(out)) = Π₁₀. Поэтому цель согласования имеет конечную форму покомпонентного равенства.
On the three roles, the same table applies: lift(encode(in)) = Π₀₀, lift(encode(∂)) = Π₀₁, lift(encode(out)) = Π₁₀. Thus the agreement target has the finite form of a componentwise equality.
↓ R-07 / частичный ответ Q-07 · ↓ Q-08 / матричное ядро · ↓ B-28 / граница утверждения
↓ R-07 / partial answer to Q-07 · ↓ Q-08 / matrix kernel · ↓ B-28 / claim boundary
Для данного четырёхсловного кода каноническая таблица назначает q00, q01, q10 и q11 проекторы Π₀₀, Π₀₁, Π₁₀ и Π₁₁ соответственно. Так дискретный слой J-29 и Matrix-слой J-28 соединены одним явным отображением.
For this four-word code, the canonical table assigns q00, q01, q10, and q11 the projectors Π₀₀, Π₀₁, Π₁₀, and Π₁₁ respectively. Thus the discrete layer J-29 and the Matrix layer J-28 are connected by one explicit map.
↓ Q-07 / открытый вопрос · ↓ A-27 / согласование · ↓ B-28 / граница
↓ Q-07 / open question · ↓ A-27 / agreement · ↓ B-28 / boundary
Статус: OPEN QUESTION. Следующая минимальная цель — определить Π00, Π01, Π10, Π11 как матрицы 4 × 4 и доказать ΠbΠc = δb,cΠc. После этого J-27 превращается в набор матричных лемм.
Status: OPEN QUESTION. The next minimal target is to define Π00, Π01, Π10, Π11 as 4 × 4 matrices and prove ΠbΠc = δb,cΠc. After that, J-27 becomes a set of matrix lemmas.
Внешние опоры повторно используются из ↓ S-37 и ↓ S-38: они дают типовой язык матриц, сопряжённого транспонирования, следа и положительной полуопределённости. Таблица lift — кандидатная конструкция этого корпуса.
External support is reused from ↓ S-37 and ↓ S-38: they provide the type language of matrices, conjugate transpose, trace, and positive semidefiniteness. The lift table is a candidate construction of this corpus.
Отдельный кандидатный файл был проверен прямым запуском в пакете HodgeFormalization. Теорема lift_encode разбирает три роли и устанавливает равенство lift(encode(role)) = encodeMatrix(role).
The separate candidate file was checked by a direct run in the HodgeFormalization package. The theorem lift_encode splits on the three roles and establishes lift(encode(role)) = encodeMatrix(role).
Проверенный объект: для каждого role : InterfaceRole теорема lift_encode возвращает lift(encode(role)) = encodeMatrix(role). Аудит `#print axioms` вывел propext, Classical.choice и Quot.sound.
Checked object: for every role : InterfaceRole, theorem lift_encode returns lift(encode(role)) = encodeMatrix(role). The `#print axioms` audit reported propext, Classical.choice, and Quot.sound.
Канонический lift из J-30 теперь имеет принятый Lean-сертификат для трёх ролей. Q-07 сохраняет открытый статус для части, где подъём должен сохранять измерительное чтение в матричном ядре.
The canonical lift from J-30 now has an accepted Lean certificate for the three roles. Q-07 keeps open status for the part where the lift must preserve measurement readout in the matrix kernel.
↓ Q-07 / открытый вопрос · ↓ Q-08 / следующий узел · ↓ B-29 / граница
↓ Q-07 / open question · ↓ Q-08 / next node · ↓ B-29 / boundary
lake env lean CANDIDATES/TLFLTwoQubitMatrixLiftCandidate.lean
'TLFLTwoQubitMatrixLiftCandidate.lift_encode'
depends on axioms: [propext, Classical.choice, Quot.sound]Локальный носитель: команда и вывод встроены как ↓ снимок аудита. Новых внешних опор для J-31 не добавлено.
Local carrier: the command and output are embedded as an ↓ audit snapshot. J-31 adds no external support.
Короткие добавления статуса: ядро ниже сохраненоCompact status additions: the core below is preserved
Черновик · исследовательская запись · рабочий журнал · кандидат. Более поздний статус добавляет контекст и сохраняет предыдущий.
Draft · research note · working journal · candidate. A later status adds context and preserves the preceding one.
К J-09 ↓To J-09 ↓Терминология переноса, топологическая инвариантность, continuation индекса и декогеренция добавлены как отдельные опоры J-08.
Transport terminology, topological invariance, index continuation, and decoherence are recorded as separate supports in J-08.
К J-08 ↓To J-08 ↓J-07 вводит кандидатное правило: рост фиксируется только вместе с переходом g_D и транспортом τ_g для инварианта домена.
J-07 introduces a candidate rule: growth is recorded only together with a transition g_D and a transport τ_g for the domain invariant.
К J-07 ↓To J-07 ↓Квантовый мост остаётся проверяемым кандидатом; к корпусу добавлены синхронизация, Lean-кандидат, контракт тела с картой и интерфейс компиляции квантовой схемы. Предыдущие статусы сохранены.
The quantum bridge remains a testable candidate; synchronization, a Lean candidate, a body-to-map contract, and a quantum-circuit compilation interface have been added to the corpus. Previous statuses are preserved.
↓ J-12 · ↓ J-13 · ↓ J-14 · ↓ J-15 · ↓ J-16Добавлены внешне опёртая линия Eₖ(σₖ) = |σₖ⟩ и один проверяемый переход T-QS-01. Стек статусов C-01 сохранён; новый носитель остаётся кандидатом.
An externally supported line Eₖ(σₖ) = |σₖ⟩ and one testable transition T-QS-01 were added. The C-01 status stack is preserved; the new carrier remains a candidate.
↓ J-17Маршрут C → Gᵣ(C) → π(C) записан как предоперационный граф для носителя |Cᵢ⟩, U и μ. Внешняя опора S-27 использована повторно; новый статус корпуса не заявляется.
The route C → Gᵣ(C) → π(C) is recorded as a pre-operational graph for the carrier |Cᵢ⟩, U, and μ. External support S-27 is reused; no new corpus status is claimed.
↓ J-18Публичный DOI добавляет проверяемую точку цитирования к сохранённому стеку статусов корпуса.
The public DOI adds a checkable citation point to the preserved stack of corpus statuses.
↓ J-19 · ↓ P-01Для носителя Γ¹∂ зафиксирован один проверяемый конечный переход α в ∂Δ²; он сохраняет три именные роли. Стек статусов C-01 сохранён, узел остаётся кандидатной рабочей проверкой.
For the carrier Γ¹∂, one checkable finite transition α into ∂Δ² is fixed; it preserves three named roles. The C-01 status stack is preserved, and the node remains a candidate working check.
↓ J-22 · ↓ A-19Для конечного барьера добавлен проверяемый язык передачи: параметры U₀, L, E и порог τ делают кандидат τtun явным. Стек статусов C-01 сохранён; это рабочий мостовой термин с отдельной границей применения.
For a finite barrier, a checkable transmission language is added: the parameters U₀, L, E, and threshold τ make the candidate τtun explicit. The C-01 status stack is preserved; this is a working bridge term with a separate boundary of application.
↓ J-23 · ↓ A-20 · ↓ B-21Критерий качества разделён на фиксированный контракт Q*, объявленное состояние свидетельств Ht и локальный рейтинг qt. Новый узел остаётся кандидатной рабочей спецификацией с открытым вопросом Q-04.
The quality criterion is separated into a fixed contract Q*, the declared evidence state Ht, and a local rank qt. The new node remains a candidate working specification with open question Q-04.
↓ J-24 · ↓ A-21 · ↓ Q-04 · ↓ B-22Это текущая карта всей работы: не новый результат, а компактная запись того, какие узлы уже собраны, что проверяется и где остаётся открытый край.
This is the current map of the whole work: not a new result, but a compact record of the nodes already assembled, what is being tested, and where the open frontier remains.
Cₜ строит Gᵣ(Cₜ); селектор задаёт gₜ. Это базовый маршрут текущего корпуса.
Cₜ constructs Gᵣ(Cₜ); a selector specifies gₜ. This is the base route of the current corpus.
Журнал хранит симплициальное различение, канал декогеренции и минимальную карточку физической системы.
The journal holds simplicial distinction, a decoherence channel, and a minimal physical-system card.
Встроенный Lean-контур хранит типы контекста, блуждания и поля ближайших целей.
The embedded Lean frame holds types for context, wandering, and the connectedness.
Q-02 требует выбрать M, правило концов и отображение в следующий симплициальный уровень.
Q-02 requires choosing M, an endpoint rule, and a map to the next simplicial level.
Здесь собраны условия, области действия и незакрытые переходы для всех утверждений страницы.
This register gathers the conditions, scopes, and open transitions for every statement on the page.
DOI подтверждает существование и цитируемость опубликованного снимка. Математические утверждения сохраняют свои отдельные источники, тесты и границы.
The DOI confirms the existence and citability of the published snapshot. Mathematical claims retain their separate sources, tests, and boundaries.
Кандидат Γ¹∂ фиксирует одну конкретную реализацию различения. Для сравнения с замкнутой окружностью, tangle или иной клеточной моделью требуется отдельный критерий эквивалентности и перенос в следующий симплициальный уровень. К A-17 ↑ · К рабочей линии R-02 ↑
The candidate Γ¹∂ fixes one concrete realization of distinction. Comparing it with a closed circle, a tangle, or another cellular model requires a separate equivalence criterion and transport to the next simplicial level. To A-17 ↑ · To working line R-02 ↑
Lean-теоремы используют как явные гипотезы сохранение кодовых слов при dephase, корректность measure и refinement физического шага. Поэтому результат является условной теоремой о формальном носителе. Динамика матриц плотности, калибровка канала, шум конкретного устройства и лабораторная реализация остаются отдельными обязательствами.
The Lean theorems use codeword preservation under dephase, correctness of measure, and refinement of the physical step as explicit hypotheses. The result is therefore a conditional theorem about a formal carrier. Density-matrix dynamics, channel calibration, concrete-device noise, and laboratory realization remain separate obligations.
A-22 фиксирует типизированную цель, но не задаёт ещё конкретные матрицы состояний, карту Φ, эффекты Pr и доказательство Target(r). До построения этих объектов запись не утверждает физическую реализацию, устойчивость к шуму конкретного устройства или выполнение Target(r) в Lean. К A-22 ↑ · К Q-05 ↑ · К J-25 ↑
A-22 fixes a typed target, but it does not yet give concrete state matrices, the map Φ, effects Pr, or a proof of Target(r). Until these objects are constructed, the entry does not claim a physical realization, device-specific noise stability, or satisfaction of Target(r) in Lean. To A-22 ↑ · To Q-05 ↑ · To J-25 ↑
A-23 задаёт один идеальный конечный носитель. Для его статуса как формального результата требуются определения всех объектов в Lean и проверка равенства следов без `sorry`. Запись не переносит этот результат на иной код, иной канал, произвольный шум или физическое устройство. К A-23 ↑ · К R-04 ↑ · К Q-05 ↑
A-23 specifies one ideal finite carrier. Its status as a formal result requires definitions of all objects in Lean and a proof of the trace equality without `sorry`. The entry does not transport this result to another code, another channel, arbitrary noise, or a physical device. To A-23 ↑ · To R-04 ↑ · To Q-05 ↑
A-24 разлагает цель на конечные равенства, но не содержит их формального Lean-доказательства, аудита аксиом или проверки отсутствия `sorry`. Равенства относятся только к одному выбранному двухкубитному коду, полной декогеренции и трёхисходному измерению; они не устанавливают устойчивость к произвольному шуму, перенос на иной носитель или физическую реализацию. К A-24 ↑ · К Q-06 ↑ · К J-27 ↑
A-24 decomposes the target into finite equalities, but it does not contain their formal Lean proof, an axiom audit, or a check for absence of `sorry`. The equalities concern only one chosen two-qubit code, complete dephasing, and a three-outcome measurement; they do not establish stability under arbitrary noise, transport to another carrier, or a physical realization. To A-24 ↑ · To Q-06 ↑ · To J-27 ↑
A-25 называет кандидатный типовой носитель, но не подтверждает, что конкретные импорты совместимы с локальной версией Lean, что API внешнего проекта подходит к нашему коду, или что файл проходит Lake build. До явной реализации, `#print axioms` и доказательства трёх равенств без `sorry` запись не является скомпилированным доказательством. К A-25 ↑ · К R-05 ↑ · К Q-06 ↑
A-25 names a candidate type carrier, but it does not establish that the concrete imports are compatible with the local Lean version, that the external project's API fits our code, or that the file passes Lake build. Until an explicit implementation, `#print axioms`, and a proof of the three equalities without `sorry`, the entry is not a compiled proof. To A-25 ↑ · To R-05 ↑ · To Q-06 ↑
A-26 фиксирует содержание локального исходного файла: его теоремы выводят устойчивое чтение и переходы только из полей StableReadoutBridge и StepRefinement. Эта запись не подтверждает запуск Lean, Lake build, аудит аксиом или отсутствие `sorry`; она также не создаёт Matrix-представление, канал CPTP или доказательство подъёма из Q-07. К A-26 ↑ · К R-06 ↑ · К Q-07 ↑
A-26 records the contents of a local source file: its theorems derive stable readout and transitions only from the fields of StableReadoutBridge and StepRefinement. This entry does not establish a Lean run, Lake build, axiom audit, or absence of `sorry`; it also does not create a Matrix representation, a CPTP channel, or a proof of the lift from Q-07. To A-26 ↑ · To R-06 ↑ · To Q-07 ↑
A-27 задаёт таблицу соответствия кодовых слов и проекторов, но не доказывает равенство lift ∘ encode = Encode внутри Lean, не задаёт элементы матриц Πb и не выводит их ортогональность. Таблица сама по себе не подтверждает CPTP-свойства Φ, формальное чтение следом или физическую реализацию. К A-27 ↑ · К R-07 ↑ · К Q-08 ↑
A-27 specifies a correspondence table between codewords and projectors, but it does not prove lift ∘ encode = Encode within Lean, define the entries of the matrices Πb, or derive their orthogonality. The table by itself does not establish the CPTP properties of Φ, formal trace readout, or a physical realization. To A-27 ↑ · To R-07 ↑ · To Q-08 ↑
A-28 подтверждает только теорему lift_encode в отдельном кандидатном файле. Аудит этой теоремы выводит три указанные логические аксиомы и не выводит `sorryAx`; он не проверяет умножение проекторов, положительность, след, канал Φ, измерение или физическую реализацию. Полная сборка пакета и аудит остальных утверждений требуют отдельных прогонов.
A-28 confirms only theorem lift_encode in a separate candidate file. The audit of this theorem reports the three listed logical axioms and does not report `sorryAx`; it does not check projector multiplication, positivity, trace, channel Φ, measurement, or a physical realization. A full package build and audits of remaining statements require separate runs.
A-19 проверяет один именованный конечный переход. Для переноса на иной носитель нужны правило эквивалентности, явное отображение α и отдельная проверка сохранения ролей; выбор общего пространства M остаётся в Q-02. К A-19 ↑ · К R-03 ↑ · К Q-02 ↑
A-19 checks one named finite transition. Transport to another carrier requires an equivalence rule, an explicit map α, and a separate role-preservation check; the choice of a general space M remains in Q-02. To A-19 ↑ · To R-03 ↑ · To Q-02 ↑
A-20 не отождествляет имеющееся отображение α с физическим туннелированием. Для такого переноса нужны отдельно заданные гамильтониан или потенциал, квантовое состояние, конечный барьер, процедура считывания и правило различения сигнала и шума. S-31 даёт внешний факт о стандартной модели барьера, но не внешнее доказательство физической реализации нашего моста. К A-20 ↑ · К J-23 ↑
A-20 does not identify the existing map α with a physical tunneling process. Such transport separately requires a specified Hamiltonian or potential, quantum state, finite barrier, readout procedure, and a rule distinguishing signal from noise. S-31 provides an external fact about the standard barrier model, not external proof of a physical realization of our bridge. To A-20 ↑ · To J-23 ↑
A-21 задаёт кандидатное разделение ролей, но не выводит универсальную норму качества и не определяет η автоматически. Для применения нужны явные типы X, E, H и q, конечное правило η, фиксированный контракт Q*, правило обновления следа и аудит, проверяющий, что qt не изменяет множество At. S-32 и S-33 служат только терминологическими опорами. К A-21 ↑ · К Q-04 ↑ · К J-24 ↑
A-21 gives a candidate role separation, but it neither derives a universal quality norm nor defines η automatically. Application requires explicit types X, E, H, and q, a finite η rule, a fixed contract Q*, a trace-update rule, and an audit checking that qt does not alter At. S-32 and S-33 serve only as terminology supports. To A-21 ↑ · To Q-04 ↑ · To J-24 ↑
Matrix m n α, конечный индекс задаётся через Fin, а сопряжённое транспонирование доступно как ᴴ.Mathlib documentation. Role: external API fact that Lean matrices are represented as Matrix m n α, with finite indices available through Fin, and that conjugate transpose is available as ᴴ. ↗ Matrix definitions · ↗ conjugate transposeРеестр текущего среза: 38 внешних опор и публичная запись P-01. S-29–S-38 добавлены с поздними журнальными узлами; P-01 добавлена с J-19.Current-slice ledger: 38 external supports and public record P-01. S-29–S-38 were added with later journal nodes; P-01 was added with J-19.
namespace TLFL
structure ContextMemory (Slice : Type u) where
pastSlices : List Slice
noisyTrace : List Slice
retained : Slice -> Prop
structure Wandering (Slice : Type u) where
step : Slice -> Slice -> Prop
structure Context (Slice : Type u) where
memory : ContextMemory Slice
current : Slice
wandering : Wandering Slice
withinSlack : Slice -> Slice -> Prop
preservesBoundary : Slice -> Prop
def nearestGoalField (C : Context Slice) : Set Slice :=
{ target |
C.wandering.step C.current target /\
C.memory.retained target /\
C.withinSlack C.current target /\
C.preservesBoundary target }
structure NearestGoal (C : Context Slice) where
target : Slice
wanderingStep : C.wandering.step C.current target
retainedByFilter : C.memory.retained target
withinAllowedSlack : C.withinSlack C.current target
preservesDistinction : C.preservesBoundary target
theorem memField (goal : NearestGoal C) :
goal.target ∈ nearestGoalField C :=
⟨goal.wanderingStep, goal.retainedByFilter,
goal.withinAllowedSlack, goal.preservesDistinction⟩
def nearestGoalOfMember
(h : target ∈ nearestGoalField C) : NearestGoal C :=
⟨target, h.1, h.2.1, h.2.2.1, h.2.2.2⟩
structure FieldOfNearestGoalsFrame (Context Action Noise : Type*) where
transition : Context -> Action -> Noise -> Context
actionAllowed : Context -> Action -> Prop
noiseAllowed : Context -> Noise -> Prop
boundary : Context -> Prop
quality : Context -> Context -> Prop
nearby : Context -> Context -> Prop
def FieldOfNearestGoals (frame : FieldOfNearestGoalsFrame Context Action Noise)
(current : Context) : Set Context :=
fun candidate =>
frame.boundary candidate /\
frame.nearby current candidate /\
frame.quality current candidate /\
∃ action, frame.actionAllowed current action /\
∃ noise, frame.noiseAllowed current noise /\
frame.transition current action noise = candidate
end TLFL
namespace TLFL
universe u
structure PhysicalInterface (State : Type u) where
System : Type u
Environment : Type u
interaction : State -> State
stable : State -> Prop
scale : Nat
F : State -> Prop
structure BridgePredicates (State : Type u) where
connected : State -> Prop
separable : State -> Prop
entangled : State -> Prop
def Distinguishes {State : Type u} (P : BridgePredicates State) : Prop :=
exists separated entangledState,
P.separable separated /\ P.entangled entangledState /\
P.connected entangledState /\ Not (P.connected separated)
structure QuantumCompilationInterface (Circuit Target Result : Type u) where
target : Target
compatible : Circuit -> Target -> Prop
transform : Circuit -> Circuit
measure : Circuit -> Result
quality : Circuit -> Prop
def QuantumAdmissible {Circuit Target Result : Type u}
(Q : QuantumCompilationInterface Circuit Target Result)
(circuit : Circuit) : Prop :=
Q.compatible circuit Q.target /\ Q.quality circuit
end TLFLВнутренний снимок самостоятельного исполнимого носителя. Он добавляет к существующему Lean-приложению отдельную последовательность для Γ¹∂.
Internal snapshot of the standalone executable carrier. It adds a separate sequence for Γ¹∂ to the existing Lean appendix.
namespace TLFL
inductive InterfaceRole where
| inside
| boundary
| outside
deriving DecidableEq, Repr
inductive TwoQubitCodeword where
| q00
| q01
| q10
| q11
deriving DecidableEq, Repr
def encode : InterfaceRole -> TwoQubitCodeword
| .inside => .q00
| .boundary => .q01
| .outside => .q10
def decode : TwoQubitCodeword -> Option InterfaceRole
| .q00 => some .inside
| .q01 => some .boundary
| .q10 => some .outside
| .q11 => none
theorem decode_encode (role : InterfaceRole) :
decode (encode role) = some role := by
cases role <;> rfl
inductive OrientedEdge : InterfaceRole -> InterfaceRole -> Prop where
| inside_boundary : OrientedEdge .inside .boundary
| boundary_outside : OrientedEdge .boundary .outside
structure StableReadoutBridge where
dephase : TwoQubitCodeword -> TwoQubitCodeword
measure : TwoQubitCodeword -> Option InterfaceRole
dephase_codeword : forall role, dephase (encode role) = encode role
measure_codeword : forall role, measure (encode role) = some role
theorem stable_readout
(bridge : StableReadoutBridge)
(role : InterfaceRole) :
bridge.measure (bridge.dephase (encode role)) = some role := by
rw [bridge.dephase_codeword role, bridge.measure_codeword role]
structure StepRefinement (bridge : StableReadoutBridge) where
physicalStep : TwoQubitCodeword -> TwoQubitCodeword
refines : forall {origin destination : InterfaceRole}, OrientedEdge origin destination ->
bridge.measure (physicalStep (encode origin)) = some destination
end TLFL