feat(Finite): add experimental Euclidean-space KetEuc and optKet

[Ruizsolveall]

Summary

This PR introduces a new experimental version of Ket (KetEuc) based on EuclideanSpace ℂ d, along with an initial example — optKet, which applies a unitary operator to a ket in this setting.

---

Motivation

The idea is to start a gradual transition from Fintype-based kets to an Euclidean-space formulation, which should make it easier to connect with Mathlib’s existing analytic tools (ContinuousLinearMap, unitary.norm_map, etc.).

Rather than modifying the existing Braket directly, this version lives in a separate file to keep things clean and avoid dependency cycles. It’s meant as a safe space to experiment and see how far we can push the Euclidean approach before integrating it more broadly.

---

Changes

• QuantumInfo.Finite.new_Braket.lean

  • Adds KetEuc: an Euclidean-space ket with the normalization condition ‖ψ‖ = 1.
  • Includes a simp lemma KetEuc.norm_one and a short alias ket for quick testing.

• QuantumInfo.Finite.UnitaryAction.lean

  • Defines optKet, showing how to apply a unitary (U ψ) using Matrix.toEuclideanLin and unitary.norm_map.

---

Notes

This is an early step toward a more analytic formulation of quantum states.
The implementation is minimal by design — the focus here is just to get a working Euclidean-space ket and demonstrate how existing proofs (like normalization preservation) adapt in this framework.

Future work can build on this structure (e.g., tensor products, inner products, or extensions toward MState).