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.
Pure loss channel and binomial thinning
An exact conditional one-mode pure-loss model with a vacuum environment mode, a passive two-mode unitary and a trace over the environment. The channel, binomial thinning and coherent-state attenuation are model deductions on the full infinite-dimensional finite-mode Fock space. No detector efficiency, actual loss record, apparatus realization, continuum bath, weak-coupling limit or experimental data are asserted.
Statement
Assume AC and , the assigned finite-mode model, one input mode and a second mode prepared independently in vacuum . Write for each one-mode Fock space and for the two-mode Fock space with ordered coordinate basis . In the completed product , define on occupation vectors, where is the two-mode occupation basis in that ordered mode basis. The product-basis result and finite-mode Fock occupation-basis result listed in Statement references make extend uniquely to a unitary . For , define and let be the two-mode beam-splitter unitary specified by the beam-splitter result in Statement references on . Transport this unitary to the product space as . Define the vacuum insertion isometry by . For every trace-class operator on , the vacuum product operator means , a trace-class operator by the trace-class ideal and tensor-map suppliers. Define where is the trace-class partial trace over the second one-mode factor. Here CPTP means complex-linear, trace-preserving, and positive after every finite-dimensional ancilla amplification on trace-class operators. The map is CPTP. For and an input number state , its output state is so ideal number detection has the binomial-thinning law. At this number input is mapped to vacuum, and at it is unchanged. For a coherent input , its output is for every . On arbitrary input states, maps to vacuum and is the identity.
Statement references
Finite-mode dipole and detector assignment
Passive beam-splitter photon statistics
Finite-mode Fock to Schrödinger identification
Separable partial trace and its basic properties
Nuclear bounded cyclicity for trace-class operators
Hilbert tensor construction: inner product, completion and product bases
Bounded tensor maps: extension, norm estimate, adjoint and commutation
Declared ideal measurements and instruments of the framework
Facts & Assumptions
Given: A one-mode trace-class input , an independent vacuum environment mode, , the passive unitary with real amplitudes , and the trace-class partial trace over the second mode.
The finite-mode assignment adopts the mode Fock spaces and ideal photon-counting model; the independent vacuum environment is a stated model preparation, not an observed state (Finite-mode dipole and detector assignment).
Assume AC for the finite-mode Bogoliubov implementation and for the trace-class partial trace and countable Fock constructions. These are mathematical assumptions, not physical postulates (The Axiom of Choice, The Axiom of Countable Choice ()).
For the passive unitary with first-column amplitudes and vacuum input on the second mode, and on the two-mode Fock space (Passive beam-splitter photon statistics). Under , these equations become and on .
For arbitrary complex Hilbert spaces , the trace-class partial trace is trace-norm contractive, preserves trace and positivity, and on rank-one tensors satisfies ; its proof assumes (Separable partial trace and its basic properties).
On trace-class operators, complete positivity means that every finite matrix amplification preserves positive trace-class block operators, and trace preservation means equality of input and output traces (Declared ideal measurements and instruments of the framework). Only these mathematical definitions are used; no measurement update is inferred.
The one-mode occupation vectors are a complete orthonormal family, and the coherent vector is normalized with expansion (Fixed-mode number law).
For trace-class and bounded , , and every trace-class input has a nuclear rank-one series convergent in trace norm (Nuclear bounded cyclicity for trace-class operators).
Bounded maps tensor to bounded maps on the completed Hilbert tensor product (Bounded tensor maps: extension, norm estimate, adjoint and commutation). For finite-dimensional , expand in an orthonormal basis of the first factor to see preserves norm whenever does; the reassociation of three factors preserves the elementary-tensor inner products and therefore extends by density to a unitary, using the completion construction (Hilbert tensor construction: inner product, completion and product bases).
Proof
For , direct multiplication gives , so the full unitary-matrix hypothesis of the beam-splitter theorem holds. The product occupation vectors form a complete orthonormal family by the product-basis result of Hilbert tensor construction: inner product, completion and product bases, and the two-mode occupation vectors form a complete orthonormal family by Finite-mode Fock to Schrödinger identification. Therefore the basis map defining preserves inner products on a dense subspace and has dense range; it extends uniquely to a surjective isometry, hence a unitary. Also, the vacuum insertion is an isometry by the elementary-tensor norm identity of Hilbert tensor construction: inner product, completion and product bases. For each finite-dimensional ancilla , is an isometry by [F6]. If is trace class, then because . For arbitrary trace-class , write as a nuclear series by [F5]. Directly from the rank-one definition and the adjoint identity, . The resulting rank-one series converges in trace norm since , and its operator-norm sum is . Since preserves inner products, [F5]'s rank-one trace formula gives . Thus adjoining vacuum is completely positive and trace-preserving.
For each finite ancilla , the amplification of the partial-trace map is, after the canonical unitary reassociation from [F6], the partial trace over the environment Fock space on . By [F2] it maps positive trace-class operators to positive trace-class operators and preserves their trace. Therefore the partial trace is completely positive and trace-preserving under [F3].
For and input , [F1] gives the joint pure state with . Expanding its rank-one density and applying the rank-one partial-trace formula [F2], cross terms with vanish because . The reduced state is , which is the displayed mixture; its ideal number-PVM law is the binomial distribution by the declared outcome model [A1].
For input , [F1] gives the product output . The rank-one partial-trace formula [F2] leaves the first factor unchanged; with , this is .
At , the transported beam-splitter expansion [F1] gives for every ; at it gives . The finite linear span of the one-mode occupation basis is dense by [F4], so boundedness of the unitaries extends these identities to and for all one-mode vectors .
Conjugation by is completely positive because unitary conjugation preserves positivity on every finite ancilla amplification. It preserves trace for every trace-class input by [F5], since ; by [F6], is unitary and the same identity holds on every finite ancilla amplification. Composition with step 1.1 preserves both properties.
By steps 1.1, 1.2 and 2.1, the composition defining maps trace-class operators to trace-class operators, is completely positive under every finite ancilla, and preserves trace. It is CPTP on the full infinite-dimensional one-mode trace-class space; no finite-dimensional Choi theorem is used.
For rank-one , the partial-trace formula [F2] applied to the two isometries in step 1.5 yields and . By [F5], every trace-class input has a nuclear series of rank-one terms converging in trace norm. The partial trace is trace-norm contractive by [F2], and bounded isometric and unitary conjugations are trace-norm continuous by [F5]; the trace is trace-norm continuous by [F5]. Passing to the limit gives and . In particular these are vacuum and identity on density operators.
Depends on
Finite-mode dipole and detector assignment
Passive beam-splitter photon statistics
Finite-mode Fock to Schrödinger identification
Separable partial trace and its basic properties
Nuclear bounded cyclicity for trace-class operators
Hilbert tensor construction: inner product, completion and product bases
Bounded tensor maps: extension, norm estimate, adjoint and commutation
Fixed-mode number law
Declared ideal measurements and instruments of the framework
The Axiom of Choice
The Axiom of Countable Choice ()