How to do No cloning theorem

Stream: Quantum information

[Ruize Chen]

Hi everyone,

I’m currently exploring the QuantumInfo library and experimenting with formalizing some simple quantum mechanical results (starting with the no-cloning theorem). I have a few questions about design choices and conventions in this part of the library.

1. Defining my own Ket in the Qubit folder
   I noticed that Ket is already defined in Braket.lean, but since Qubit.lean starts from unitary matrices (rather than abstract Hilbert-space elements), I’m working directly at the “matrix level.”
   From a generalization perspective, I thought it might make sense to define a simple Ket := Matrix Qubit (Fin 1) ℂ locally, so that I can directly combine it with the existing unitaries.
   Since I’m new to working with an evolving library, I’d like to ask whether this approach is acceptable—or whether I should try to interface directly with the Braket version instead.

2. Defining a custom inner product
   I noticed that Qubit.lean defines the operators (X, Y, Z, etc.) but doesn’t provide any notion of an inner product.
   I therefore defined a minimal version for column vectors:

    def spBra (ψ : ket) : Matrix (Fin 1) Qubit ℂ := ψ.conjTranspose
    noncomputable def qbbraket (φ ψ : ket) : ℂ := (spBra φ * ψ) 0 0

I’m aware that Braket.lean already defines a more expressive dot operation, but I wanted a lightweight definition to get basic examples working and to evaluate whether it’s worth integrating at the Qubit level.
Is it reasonable to do this, or should I instead rely on the Braket abstractions?

3. Tensor product ambiguity between Matrix.kronecker and CPTPMap
   When I use ⊗ₖ in a theorem (even after explicitly open Kronecker), Lean reports an ambiguity between Matrix.kronecker and CPTPMap.
   Since my current goal is purely linear-algebraic (no channels or CPTP maps involved), I’d like to confirm:

   - Am I expected to use CPTPMap in this context?

   - If not, what’s the cleanest way to force Lean to interpret ⊗ₖ as the matrix version throughout this file?

Thanks a lot for your time — I just want to make sure I’m following the right design philosophy before building too much on top of my local definitions.
You can find my naive work attached, plz open it in the repo.
no cloning.lean

[Alex Meiburg]

Hi! First thing, I would note that we recently got a version of no cloning: https://github.com/Timeroot/Lean-QuantumInfo/blob/6806c6483ddfbb66beb9c6056e8ae72a1ddace7e/QuantumInfo/Finite/Unitary.lean#L76
but there's definitely room for more, since there are so many (really different) versions of the no-cloning theorem.

I would definitely encourage you to try to use the existing types where possible. If you prove a version of no-cloning with your spBra and qbbraket, for instance, then it will make it harder for anyone else to use your theorem in downstream proofs, since they'll have to show that their existing hypotheses (like about an inner product of a Bra and Ket) are equivalent to your h3 about qbbraket. And they won't be able to apply your version to an actual Ket without casting.

[Alex Meiburg]

Regarding the Matrix.kronecker and CPTPMap: I guess the ⊗ₖ notation for CPTP maps should be scoped. I've also been thinking about changing it to something less ambiguous from the start.

There's a bit of a mess because we have kronecker product of Matrix, of HermitianMat, of MState, of Ket, and of CPTPMap. (Also need to get one for unitaries.) The elaborator gets a bit confused sometimes.

I would encourage you to try to state it entirely in terms of Ket or MState, and in terms of 𝐔 or CPTPMap, depending on what version of the theorem you want to prove. Hopefully you can avoid the notation collision then.

A simple workaround is to just explicitly name the function, e.g. CPTPMap.prod, if you need to.

[Ruize Chen]

I see, thank you for sharing this. My intention to do this theorem is just to practice and learn the ways people deal with matrices. I will read about the existing code thank you.

[Ruize Chen]

I think I didn’t get the way operators interact with the existing Ket. That was why I didn’t use the existing def. I get it now. Cheers

[Alex Meiburg]

Oh, shoot. Yes, there's an embarrassing fact that we don't actually have the multiplication of a unitary by a ket. (In particular, showing that it's still a ket - still correctly normalized.) @Mattias Ehatamm pointed this out to me a few days ago.

[Ruize Chen]

Thanks! That clarifies a lot.
I saw the TODO in the current Ket definition about switching to EuclideanSpace ℂ d, and it helped me understand why the normalization proof isn’t straightforward right now — that change would naturally make normalization follow from unitarity, since the inner-product structure would already be built in.
I’ve been experimenting locally with a small version to see how the unitary–Ket multiplication could take advantage of that TODO and fit into the updated design — mainly to learn how things connect inside the library.

Out of curiosity, do you think the plan is to update Ket itself soon, or is the idea to focus on adding operators first before that change?

[Alex Meiburg]

I'm not sure... at the moment there's a lot of tech debt in the repo, as we've been pushing for a deadline to get the Stein's Lemma done. We're pretty much closing that up, and then it will be time to start tackling all of these TODO's and tech debts. Switching to EuclideanSpace will probably be an early one. You should expect it in like, a month from now? I would guess.

[Ruize Chen]

That makes total sense — thanks for the context!
Sounds like a good time for me to just keep experimenting locally and get familiar with how things are structured.
I’ll revisit once the EuclideanSpace update lands; it’ll be nice to see how the operator fits into that new setup.

[Ruize Chen]

Quick update on the experiment I mentioned earlier:

I tried implementing the TODO version of Ket (with vec : EuclideanSpace ℂ n) and wrote a preliminary version of the unitary–Ket multiplication (opKet).
Since there isn’t yet a direct matrix multiplication API for this, I constructed the corresponding unitary (EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d) explicitly from U : Matrix.unitaryGroup d ℂ and used unitary.norm_map to prove the normalization.

I’d be happy to refine it later once the EuclideanSpace-based Ket update lands — this was mainly a learning exercise to see how all the existing structures connect together.

Here is the code. Special Thanks to Andrew Yang for his tips in this proof.

new_opt_multi.lean