Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Broadcasting channels need have neither extremum

Abstract

A three-dimensional observable with two outcomes has a nonempty set of broadcasting channels and has neither extremum under nondisturbing precomposition.

Theorem 1.1 (Density matrices are contractions).

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.density_le_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every positive semidefinite complex matrix of trace one is bounded above by the identity in the positive semidefinite order.

Definition 1.2 (Finite Kraus channels).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.IsChannel (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Section II.B, p. 2: “A CPTP map Θ : S(Hin) → S(Hout) is called a quantum channel, where Hin and Hout are two Hilbert spaces [15].” Finite Kraus form expresses complete positivity and trace preservation. MatrixMap.of_kraus is the frozen operation; its action is the finite sum of K(j) X conjTranspose(K(j)). The output index type iota has anonymous Fintype and DecidableEq instances.

Definition 1.3 (Broadcasting an observable).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.Broadcasts (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Definition 1, p. 2: “A channel Λ : S(H) → S(H_A ⊗ H_B) with H_A = H_B = H is called a broadcasting channel.” Definition 3, p. 3: “An observable A ∈ O_X^d is broadcast by a broadcasting channel Λ ∈ C_broad^d if for all ρ ∈ S(H), x ∈ X” followed by equation (5), Tr[ρA(x)] = Tr[Λ(ρ)A(x) ⊗ I] = Tr[Λ(ρ)I ⊗ A(x)]. Outcomes are Fin m, and each subsystem is indexed by Fin d. The state predicate is the SLDSpectralEnergy.IsDensity: positive semidefinite with trace one.

Definition 1.4 (Nondisturbing channels).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.Nondisturbing (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Definition 8, p. 5: “A channel Θ : S(H) → S(H) is nondisturbing with respect to an observable A if for all ρ ∈ S(H),” followed by equation (22), Tr[ρA(x)] = Tr[Θ(ρ)A(x)] for all x ∈ Ω_A. The displayed formula uses this trace form, equivalent to the dual form in equation (23).

Definition 1.5 (Nondisturbing precomposition).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.ConstructedFrom (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Section III.A, p. 5 uses concatenation with nondisturbing channels. ConstructedFrom A Lprime L states that Lprime = L ∘ Theta for such a channel Theta. Equality is equality on all complex matrices.

Definition 1.6 (Highest element).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.HasHighest (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Section III.A, p. 5: “For an observable, in this way, one can get the set of different broadcasting channels that broadcast the observable. It is an open question whether this set has the highest element i.e., a broadcasting channel in this set from which all other broadcasting channels that can broadcast the observable, can be constructed through concatenation with nondisturbing channels. It is also an open question whether this set has the lowest element i.e., a broadcasting channel in this set which can be constructed from all other broadcasting channels that broadcast the observable through concatenation with nondisturbing channels.” HasHighest requires a broadcasting channel H from which every broadcasting channel L is obtained by nondisturbing precomposition.

Definition 1.7 (Lowest element).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.HasLowest (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Section III.A, p. 5: “For an observable, in this way, one can get the set of different broadcasting channels that broadcast the observable. It is an open question whether this set has the highest element i.e., a broadcasting channel in this set from which all other broadcasting channels that can broadcast the observable, can be constructed through concatenation with nondisturbing channels. It is also an open question whether this set has the lowest element i.e., a broadcasting channel in this set which can be constructed from all other broadcasting channels that broadcast the observable through concatenation with nondisturbing channels.” HasLowest requires a broadcasting channel H obtained from every broadcasting channel L by nondisturbing precomposition.

Definition 1.8 (The two extremum questions).

Formalization. D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.claim (✓ std3).

Citation. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Section III.A, p. 5: “For an observable, in this way, one can get the set of different broadcasting channels that broadcast the observable. It is an open question whether this set has the highest element i.e., a broadcasting channel in this set from which all other broadcasting channels that can broadcast the observable, can be constructed through concatenation with nondisturbing channels. It is also an open question whether this set has the lowest element i.e., a broadcasting channel in this set which can be constructed from all other broadcasting channels that broadcast the observable through concatenation with nondisturbing channels.” The universal encoding quantifies over natural dimensions d, outcome counts m, and all observables A. The frozen ConcealmentKernelNecessityRefutation.IsPOVM means that every effect is positive semidefinite and their sum is I. Nonemptiness of the broadcasting set is explicit. The disjunction allows either extremum; its negation exhibits one observable lacking both.

Theorem 1.9 (Both answers can be negative).

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.result (✓ std3). ∎

Resolves. Problems/mitra-2021-broadcasting-channel-extrema (refuted) by D5/S3/Quantum/Measurements/BroadcastingChannelExtremaRefutation.result.

Source. Repository-derived.

Acknowledgement. A. Mitra (2021). Layers of classicality in the compatibility of measurements. DOI: 10.1103/PhysRevA.104.022206. URL: https://arxiv.org/abs/2101.05752v4.

Commentary.

Take d = 3, m = 2, P = diag(1,1,0), Q = I − P, A(0) = (3/4)P + (1/4)Q, and A(1) = I − A(0). Three broadcasting channels prepare the matrix units at (0,0), (1,1), and (0,1) on the P sector and at (2,2) on the Q sector. Preservation of A(0) and trace forces preservation of P. ConcealmentKernelNecessityRefutation.dual_kraus identifies the dual effect. The balanced state on coordinates zero and two is ActualQubitChordObstruction.signalProbe 1. Together with the other normalized real and imaginary pure states it determines the dual effect on all matrices, so nondisturbing precomposition fixes each of the three channels. Their inequality excludes a lowest element. FiniteMemoryHistoryCapacity.zero_trace_mul_eq_zero applied to I − P places the three input states of a highest element in the P sector. They would produce three orthogonal pure outputs. Positivity and the dual Kraus completeness identity bound their total trace by trace(P) = 2, although each output contributes at least one. Thus 3 ≤ 2, a contradiction. Only this three-dimensional, two-outcome instance is asserted; the rank-r family and the qubit and sharp-observable questions remain open here.

References