LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Exact logical-block correctness forces zero leakage

Statement

Let $J : C \to V$ be an isometric encoding with $P = J J^{*}$ , let $U$ be unitary on $C$ , and let $W$ be unitary on $V$ . If the logical block error $∥ P W P - J U J^{*} ∥_{o p}$ is zero, then the leakage amplitude $∥ (I - P) W P ∥_{o p}$ is zero.

Facts & Assumptions

Given: Finite-dimensional inner-product spaces $C, V$ , an isometry $J : C \to V$ , a unitary $U$ on $C$ , a unitary $W$ on $V$ , and zero logical block error.

[F1]

The logical block error is $∥ P W P - J U J^{*} ∥_{o p}$ and the leakage amplitude is $∥ (I - P) W P ∥_{o p}$ ; $P = J J^{*}$ is the orthogonal projection onto $J C$ . Logical block error and leakage amplitude

[F2]

Isometries preserve inner-product norm, and orthogonal projection splits a vector into orthogonal code and complement components. Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product

Proof

1.1givenF1F2algebra

Zero block error means $P W P = J U J^{*}$ as operators on $V$ . For every $x \in C$ , $J^{*} J = I_{C}$ gives $P W J x = P W P J x = J U J^{*} J x = J U x$ . By [F2], $∥ W J x ∥ = ∥ x ∥$ and $∥ P W J x ∥ = ∥ J U x ∥ = ∥ U x ∥ = ∥ x ∥$ .

2.1F1F2step 1.1algebra∎

The decomposition $W J x = P W J x + (I - P) W J x$ is orthogonal by [F1]. Its Pythagorean identity and step 1.1 give $∥ (I - P) W J x ∥^{2} = ∥ W J x ∥^{2} - ∥ P W J x ∥^{2} = 0$ for every $x$ . Hence $(I - P) W J = 0$ , and since $P = J J^{*}$ , $(I - P) W P = 0$ ; its operator norm is zero.

Depends on

Used by

B6 exact rank certificates and encoded leakage budget Example

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Chetan Nayak, Steven H. Simon, Ady Stern, Michael Freedman, and Sankar Das Sarma, Non-Abelian Anyons and Topological Quantum Computation (standard reference, not scraped)