Guidance on preparing a PR for the EuclideanSpace-based Ket

Stream: Quantum information

[Ruize Chen]

Hi everyone,

I’ve been working on the EuclideanSpace-based version of Ket (following the TODO in the current definition),
and managed to get both versions of the optKet proof working —
one for the current Ket (vec : d → ℂ), and one for the updated EuclideanSpace-based version (vec : EuclideanSpace ℂ d).

The two proofs are quite similar, so I’ve placed them in the same file for now.
I’d love to prepare a small PR for this, but since it would be my first contribution to QuantumInfo,
I wanted to ask for a bit of guidance on the process and best practices (e.g. file placement, naming, comments).

Also, I currently use a few erw steps to handle coercions between LinearMap and ContinuousLinearMap,
so if there’s a more idiomatic way to express those using the existing API, I’d be very happy to learn it.

Would it make sense to open a draft PR and iterate from there?
Or would you prefer I wait until the EuclideanSpace refactor starts and contribute it to that branch instead?

Thanks again for leaving that TODO note — it made the design direction very clear!

Here is the file
new_opt_multi_KET.lean

[Alex Meiburg]

Since it looks like you've already made a good stab, I would say open a PR! This could be the EuclideanSpace definition then. It can be a draft PR, sure. In your PR, I would replace the existing Ket with the EuclideanSpace definition, and add these theorems you have.

This will definitely break some other theorems, that's ok. Of course fix anything you see how to fix easily, go ahead, but it's okay if it's not everything; then we can look over improving it

[Ruize Chen]

Thanks, Alex — I’ll go ahead and start on this then!

I’ve looked through Braket.lean and did a quick assessment of the changes —
most of the adjustments seem to be type-level issues rather than anything deep mathematically,
so I think it’s manageable overall.

That said, I also prepared an optKet for the current definition (the existing vec : d → ℂ version),
so if fixing all the dependent lemmas turns out to be a bit heavy,
you’re very welcome to use that one directly from my file as a fallback —
it might help maintain compatibility while still adding the missing definition.

Thanks again for offering to handle the follow-up fixes — I really appreciate it!

[Alex Meiburg]

I guess I would:

• rename the old Ket to something like KetOld, and change it everywhere
• Add the new Ket alongside it
• Add a depreciation notice (mathlib has many examples of these) to KetOld. It will be removed eventually
• Change any KetOld theorems to Ket that you can. For now, that might mean keeping both around.
• If you change a KetOld theorem to Ket and nothing else relies on it (no other KetOld theorems need it), then we can just delete it

[Alex Meiburg]

That way we won't introduce new sorries.

Then I can take a look at helping get rid of remaining KetOld stuff.

[Ruize Chen]

Hi Alex,

I followed your suggestion about replacing the old Ket references with KetOld and defining a new Ket alongside.
After trying it out, I realised the approach quickly becomes tangled — mainly because MState and a few other modules depend directly on names like Ket.apply and Ket.prod. Even with the alias in place, Lean still looks for those symbols under the new namespace, so we’d have to maintain a compatibility layer that could get messy over time.

Based on that, I think it’s cleaner to start a fully isolated file (say NewKet.lean) for the Euclidean-space implementation. This keeps the prototype self-contained, avoids breaking dependencies, and lets us migrate to it cleanly once it’s stable.

My impression is that this approach fits better with the long-term structure of the repo — and it avoids the half-patched state that a temporary alias would create.

For now, I don’t plan to add too much inside NewKet.lean; I will start by adding what I have in the file I sent above into the isolated NewKet.lean, and I think similar construction (gonna be the same as Braket.lean, I believe it's gonna be fast because we have the old one as good guidance) can begin in the isolated file.

Does that sound good to you? I can push the first draft of NewKet.lean once everything compiles cleanly.

[Alex Meiburg]

Mm, I guess I feel like it's not good to have a second file and stuff. if you feel it's too tough to get all those other changes (like Ket.apply) then let's just skip the deprecation and go straight to the new one.

You can make the PR, it will have a lot of code not working, that's ok. I'll take a look

[Ruize Chen]

Ah got it — just to explain a bit what I was trying to do:
I mainly wanted to update optKet in a “smarter” way, basically to directly write the Euclidean version that works with both Unitary and Braket.
That’s why it really needed its own file — it sits between the two and would easily cause dependency cycles otherwise.

While doing that, I realized the Braket side itself also needed to be Euclideanized, so I added a minimal KetEuc definition just to make optKet compile cleanly and test the setup.

The idea was never to maintain two versions permanently — just to isolate the new logic until it’s good enough to replace the old one entirely.

If you’d prefer doing the replacement directly inside the same file instead, I can take care of that — I’ll just use a regex pass to systematically rename all Ket to KetOld in Braket.lean to the new version.
I’ll likely do that tomorrow once I’ve confirmed everything still builds properly.

[Alex Meiburg]

Sure, yeah. Let's just skip the KetOld completely and just remove it right away.