diff --git a/Cslib.lean b/Cslib.lean
index eea1f4491..3a4735657 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -37,6 +37,9 @@ public import Cslib.Computability.Languages.OmegaLanguage
 public import Cslib.Computability.Languages.OmegaRegularLanguage
 public import Cslib.Computability.Languages.RegularLanguage
 public import Cslib.Computability.Machines.Turing.SingleTape.Deterministic
+public import Cslib.Computability.Quantum.Gate
+public import Cslib.Computability.Quantum.Register
+public import Cslib.Computability.Quantum.State
 public import Cslib.Computability.URM.Basic
 public import Cslib.Computability.URM.Computable
 public import Cslib.Computability.URM.Defs
diff --git a/Cslib/Computability/Quantum/Gate.lean b/Cslib/Computability/Quantum/Gate.lean
new file mode 100644
index 000000000..24b9b64ff
--- /dev/null
+++ b/Cslib/Computability/Quantum/Gate.lean
@@ -0,0 +1,495 @@
+/-
+Copyright (c) 2026 QudeLeap. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: QudeLeap Team
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Computability.Quantum.State
+public import Mathlib.LinearAlgebra.UnitaryGroup
+public import Mathlib.LinearAlgebra.Matrix.Permutation
+
+/-!
+# Hilbert operators and unitary gates over finite registers
+
+`HilbertOperator R` is the raw complex matrix over a finite register `R`.
+It is used for observables, projectors, matrix sums, and block-encoding targets
+that are not necessarily unitary.
+
+`Gate R` is a unitary Hilbert operator.  A gate acts on raw vectors by
+`applyVec` and evolves pure states by `apply`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+/-- Raw linear operator over a finite quantum register. -/
+abbrev HilbertOperator (R : Register) : Type := Matrix R.Index R.Index ℂ
+
+namespace HilbertOperator
+
+noncomputable section
+
+variable {R : Register}
+
+/-- A Hilbert operator acts on a raw state vector by matrix-vector multiplication. -/
+def applyVec (A : HilbertOperator R) (psi : StateVector R) : StateVector R :=
+  WithLp.toLp 2 (A.mulVec psi.ofLp)
+
+@[simp]
+theorem applyVec_apply (A : HilbertOperator R) (psi : StateVector R) (i : R.Index) :
+    applyVec A psi i = ∑ j, A i j * psi j :=
+  rfl
+
+@[simp]
+theorem applyVec_add (A : HilbertOperator R) (psi phi : StateVector R) :
+    applyVec A (psi + phi) = applyVec A psi + applyVec A phi := by
+  unfold applyVec
+  rw [show (psi + phi).ofLp = psi.ofLp + phi.ofLp from rfl, Matrix.mulVec_add]
+  rfl
+
+@[simp]
+theorem applyVec_sub (A : HilbertOperator R) (psi phi : StateVector R) :
+    applyVec A (psi - phi) = applyVec A psi - applyVec A phi := by
+  unfold applyVec
+  rw [show (psi - phi).ofLp = psi.ofLp - phi.ofLp from rfl, Matrix.mulVec_sub]
+  rfl
+
+@[simp]
+theorem applyVec_smul (A : HilbertOperator R) (c : ℂ) (psi : StateVector R) :
+    applyVec A (c • psi) = c • applyVec A psi := by
+  unfold applyVec
+  rw [show (c • psi).ofLp = c • psi.ofLp from rfl, Matrix.mulVec_smul]
+  rfl
+
+@[simp]
+theorem applyVec_neg (A : HilbertOperator R) (psi : StateVector R) :
+    applyVec A (-psi) = -applyVec A psi := by
+  unfold applyVec
+  rw [show (-psi).ofLp = -psi.ofLp from rfl, Matrix.mulVec_neg]
+  rfl
+
+@[simp]
+theorem add_applyVec (A B : HilbertOperator R) (psi : StateVector R) :
+    applyVec (A + B) psi = applyVec A psi + applyVec B psi := by
+  unfold applyVec
+  rw [Matrix.add_mulVec]
+  rfl
+
+@[simp]
+theorem smul_applyVec (c : ℂ) (A : HilbertOperator R) (psi : StateVector R) :
+    applyVec (c • A) psi = c • applyVec A psi := by
+  unfold applyVec
+  rw [Matrix.smul_mulVec]
+  rfl
+
+@[simp]
+theorem one_applyVec (psi : StateVector R) : applyVec (1 : HilbertOperator R) psi = psi := by
+  unfold applyVec
+  rw [Matrix.one_mulVec]
+
+theorem mul_applyVec (A B : HilbertOperator R) (psi : StateVector R) :
+    applyVec (A * B) psi = applyVec A (applyVec B psi) := by
+  unfold applyVec
+  rw [show (WithLp.toLp 2 (B.mulVec psi.ofLp)).ofLp = B.mulVec psi.ofLp from rfl,
+    Matrix.mulVec_mulVec]
+
+/-- A Hilbert operator sends a basis ket to its corresponding column. -/
+theorem applyVec_ket (A : HilbertOperator R) (x : R.Index) (i : R.Index) :
+    applyVec A (PureState.ket x : StateVector R) i = A i x := by
+  rw [applyVec_apply]
+  simp only [PureState.ket_apply, mul_ite, mul_one, mul_zero]
+  exact Fintype.sum_ite_eq' x (fun j => A i j)
+
+/-- Hilbert operators are equal when they agree on all state vectors. -/
+theorem ext_of_applyVec_eq {A B : HilbertOperator R}
+    (h : ∀ psi : StateVector R, applyVec A psi = applyVec B psi) :
+    A = B := by
+  ext i j
+  have hket := congrArg (fun psi : StateVector R => psi i)
+    (h (PureState.ket j : StateVector R))
+  simpa using hket
+
+/-- Applying a Hilbert operator to a finite sum of state vectors is the finite
+sum of its applications. -/
+theorem applyVec_sum {ι : Type} [Fintype ι]
+    (A : HilbertOperator R) (f : ι → StateVector R) :
+    applyVec A (∑ i, f i) = ∑ i, applyVec A (f i) := by
+  classical
+  refine Finset.induction_on (Finset.univ : Finset ι) ?_ ?_
+  · ext k
+    simp [applyVec_apply]
+  · intro i s hi ih
+    simp [Finset.sum_insert, hi, applyVec_add, ih]
+
+/-- Applying a finite sum of Hilbert operators is the finite sum of their
+applications. -/
+theorem sum_applyVec {ι : Type} [Fintype ι]
+    (f : ι → HilbertOperator R) (psi : StateVector R) :
+    applyVec (∑ i, f i) psi = ∑ i, applyVec (f i) psi := by
+  classical
+  refine Finset.induction_on (Finset.univ : Finset ι) ?_ ?_
+  · ext k
+    simp [applyVec_apply]
+  · intro i s hi ih
+    simp [Finset.sum_insert, hi, add_applyVec, ih]
+
+/-- Hilbert operators are equal when they agree on every vector of an
+orthonormal basis. -/
+theorem ext_of_applyVec_eq_on_orthonormalBasis {ι : Type} [Fintype ι]
+    (basis : OrthonormalBasis ι ℂ (StateVector R))
+    {A B : HilbertOperator R}
+    (h : ∀ i : ι, applyVec A (basis i) = applyVec B (basis i)) :
+    A = B := by
+  apply ext_of_applyVec_eq
+  intro psi
+  calc
+    applyVec A psi =
+        applyVec A (∑ i, basis.repr psi i • basis i) := by
+          rw [basis.sum_repr]
+    _ = ∑ i, applyVec A (basis.repr psi i • basis i) := by
+          rw [applyVec_sum]
+    _ = ∑ i, basis.repr psi i • applyVec A (basis i) := by
+          simp [applyVec_smul]
+    _ = ∑ i, basis.repr psi i • applyVec B (basis i) := by
+          exact Finset.sum_congr rfl fun i _ => by rw [h i]
+    _ = ∑ i, applyVec B (basis.repr psi i • basis i) := by
+          simp [applyVec_smul]
+    _ = applyVec B (∑ i, basis.repr psi i • basis i) := by
+          rw [applyVec_sum]
+    _ = applyVec B psi := by
+          rw [basis.sum_repr]
+
+/-- A unitary Hilbert operator preserves inner products on raw state vectors. -/
+theorem inner_applyVec_applyVec_of_mem_unitaryGroup {U : HilbertOperator R}
+    (hU : U ∈ Matrix.unitaryGroup R.Index ℂ) (psi phi : StateVector R) :
+    inner ℂ (applyVec U psi) (applyVec U phi) = inner ℂ psi phi := by
+  have hUU : U.conjTranspose * U = 1 := by
+    rw [← Matrix.star_eq_conjTranspose]
+    exact Matrix.mem_unitaryGroup_iff'.mp hU
+  simp only [PiLp.inner_apply, RCLike.inner_apply, applyVec_apply]
+  calc ∑ i, (∑ k, U i k * phi k) * starRingEnd ℂ (∑ j, U i j * psi j)
+      = ∑ i, ∑ k, ∑ j, (U i k * starRingEnd ℂ (U i j))
+          * (phi k * starRingEnd ℂ (psi j)) := by
+        refine Finset.sum_congr rfl fun i _ => ?_
+        rw [map_sum, Finset.sum_mul_sum]
+        refine Finset.sum_congr rfl fun k _ =>
+          Finset.sum_congr rfl fun j _ => ?_
+        rw [map_mul]
+        ring
+    _ = ∑ k, ∑ j, (∑ i, U i k * starRingEnd ℂ (U i j))
+          * (phi k * starRingEnd ℂ (psi j)) := by
+        rw [Finset.sum_comm]
+        refine Finset.sum_congr rfl fun k _ => ?_
+        rw [Finset.sum_comm]
+        refine Finset.sum_congr rfl fun j _ => ?_
+        rw [Finset.sum_mul]
+    _ = ∑ k, ∑ j, (1 : HilbertOperator R) j k * (phi k * starRingEnd ℂ (psi j)) := by
+        refine Finset.sum_congr rfl fun k _ =>
+          Finset.sum_congr rfl fun j _ => ?_
+        congr 1
+        rw [← hUU, Matrix.mul_apply]
+        exact Finset.sum_congr rfl fun i _ => by
+          rw [Matrix.conjTranspose_apply,
+            show star (U i j) = starRingEnd ℂ (U i j) from rfl, mul_comm]
+    _ = ∑ k, phi k * starRingEnd ℂ (psi k) := by
+        refine Finset.sum_congr rfl fun k _ => ?_
+        simp only [Matrix.one_apply, ite_mul, one_mul, zero_mul]
+        exact Fintype.sum_ite_eq' k fun j => phi k * starRingEnd ℂ (psi j)
+
+/-- A unitary Hilbert operator preserves raw vector norms. -/
+theorem norm_applyVec_of_mem_unitaryGroup {U : HilbertOperator R}
+    (hU : U ∈ Matrix.unitaryGroup R.Index ℂ) (psi : StateVector R) :
+    ‖applyVec U psi‖ = ‖psi‖ := by
+  have h := inner_applyVec_applyVec_of_mem_unitaryGroup hU psi psi
+  rw [inner_self_eq_norm_sq_to_K, inner_self_eq_norm_sq_to_K] at h
+  have h2 : ‖applyVec U psi‖ ^ 2 = ‖psi‖ ^ 2 := by exact_mod_cast h
+  calc ‖applyVec U psi‖ = Real.sqrt (‖applyVec U psi‖ ^ 2) :=
+        (Real.sqrt_sq (norm_nonneg _)).symm
+    _ = Real.sqrt (‖psi‖ ^ 2) := by rw [h2]
+    _ = ‖psi‖ := Real.sqrt_sq (norm_nonneg _)
+
+end
+
+end HilbertOperator
+
+/-- A unitary gate over a finite quantum register. -/
+structure Gate (R : Register) where
+  /-- Underlying Hilbert-space operator. -/
+  op : HilbertOperator R
+  /-- Gates are unitary by definition. -/
+  unitary : op ∈ Matrix.unitaryGroup R.Index ℂ
+
+namespace Gate
+
+noncomputable section
+
+variable {R : Register}
+
+instance : Coe (Gate R) (HilbertOperator R) := ⟨Gate.op⟩
+instance : CoeTail (Gate R) (HilbertOperator R) := ⟨Gate.op⟩
+instance : CoeOut (Gate R) (HilbertOperator R) := ⟨Gate.op⟩
+
+instance : CoeFun (Gate R) (fun _ => R.Index → R.Index → ℂ) :=
+  ⟨fun G => G.op⟩
+
+instance : HMul (Gate R) (HilbertOperator R) (HilbertOperator R) where
+  hMul G A := (G : HilbertOperator R) * A
+
+instance : HMul (HilbertOperator R) (Gate R) (HilbertOperator R) where
+  hMul A G := A * (G : HilbertOperator R)
+
+@[ext]
+theorem ext {G K : Gate R} (h : ∀ i j, G i j = K i j) : G = K := by
+  cases G with
+  | mk G hG =>
+    cases K with
+    | mk K hK =>
+      have hGK : G = K := by
+        ext i j
+        exact h i j
+      subst hGK
+      rfl
+
+/-- Build a gate from a unitary Hilbert operator. -/
+def ofUnitary (U : HilbertOperator R)
+    (hU : U ∈ Matrix.unitaryGroup R.Index ℂ) : Gate R := ⟨U, hU⟩
+
+@[simp]
+theorem coe_ofUnitary (U : HilbertOperator R)
+    (hU : U ∈ Matrix.unitaryGroup R.Index ℂ) :
+    ((ofUnitary U hU : Gate R) : HilbertOperator R) = U := rfl
+
+instance : Monoid (Gate R) where
+  one := ofUnitary 1 (one_mem _)
+  mul G K := ofUnitary ((G : HilbertOperator R) * (K : HilbertOperator R))
+    (mul_mem G.unitary K.unitary)
+  one_mul G := by
+    ext i j
+    change ((1 : HilbertOperator R) * (G : HilbertOperator R)) i j = G i j
+    simp
+  mul_one G := by
+    ext i j
+    change ((G : HilbertOperator R) * (1 : HilbertOperator R)) i j = G i j
+    simp
+  mul_assoc G K L := by
+    ext i j
+    change (((G : HilbertOperator R) * (K : HilbertOperator R)) * (L : HilbertOperator R)) i j
+      = ((G : HilbertOperator R) * ((K : HilbertOperator R) * (L : HilbertOperator R))) i j
+    rw [Matrix.mul_assoc]
+
+@[simp]
+theorem coe_one : (((1 : Gate R) : HilbertOperator R)) = 1 := rfl
+
+@[simp]
+theorem coe_mul (G K : Gate R) :
+    (((G * K : Gate R) : HilbertOperator R))
+      = (G : HilbertOperator R) * (K : HilbertOperator R) := rfl
+
+@[simp]
+theorem coe_pow (G : Gate R) (k : ℕ) :
+    (((G ^ k : Gate R) : HilbertOperator R)) =
+      (G : HilbertOperator R) ^ k := by
+  induction k with
+  | zero => rfl
+  | succ k ih =>
+      simp [pow_succ, ih]
+
+/-- Conjugate transpose of a unitary gate, again as a gate. -/
+def conjTranspose (G : Gate R) : Gate R :=
+  ofUnitary ((G : HilbertOperator R).conjTranspose) (by
+    rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose,
+      Matrix.conjTranspose_conjTranspose]
+    exact Matrix.mem_unitaryGroup_iff'.mp G.unitary)
+
+instance : Inv (Gate R) := ⟨conjTranspose⟩
+
+@[simp]
+theorem coe_conjTranspose (G : Gate R) :
+    ((G.conjTranspose : Gate R) : HilbertOperator R)
+      = (G : HilbertOperator R).conjTranspose := rfl
+
+/-- A gate acts on a raw vector by its underlying Hilbert operator. -/
+def applyVec (G : Gate R) (psi : StateVector R) : StateVector R :=
+  HilbertOperator.applyVec (G : HilbertOperator R) psi
+
+/-- A gate evolves a pure state to a pure state. -/
+def apply (G : Gate R) (psi : PureState R) : PureState R :=
+  PureState.ofVec (G.applyVec (psi : StateVector R)) (by
+    change ‖HilbertOperator.applyVec (G : HilbertOperator R) (psi : StateVector R)‖ = 1
+    rw [HilbertOperator.norm_applyVec_of_mem_unitaryGroup G.unitary, psi.norm_eq_one])
+
+/-- Alias for `apply`, emphasizing unitary time evolution. -/
+def evolve (G : Gate R) (psi : PureState R) : PureState R := G.apply psi
+
+@[simp]
+theorem apply_coe (G : Gate R) (psi : PureState R) :
+    ((G.apply psi : PureState R) : StateVector R) = G.applyVec (psi : StateVector R) := rfl
+
+@[simp]
+theorem applyVec_apply (G : Gate R) (psi : StateVector R) (i : R.Index) :
+    G.applyVec psi i = ∑ j, G i j * psi j := rfl
+
+theorem apply_apply (G : Gate R) (psi : PureState R) (i : R.Index) :
+    G.apply psi i = ∑ j, G i j * psi j := by
+  change G.applyVec (psi : StateVector R) i = ∑ j, G i j * psi j
+  rfl
+
+@[simp]
+theorem applyVec_add (G : Gate R) (psi phi : StateVector R) :
+    G.applyVec (psi + phi) = G.applyVec psi + G.applyVec phi :=
+  HilbertOperator.applyVec_add (G : HilbertOperator R) psi phi
+
+@[simp]
+theorem applyVec_sub (G : Gate R) (psi phi : StateVector R) :
+    G.applyVec (psi - phi) = G.applyVec psi - G.applyVec phi :=
+  HilbertOperator.applyVec_sub (G : HilbertOperator R) psi phi
+
+@[simp]
+theorem applyVec_smul (G : Gate R) (c : ℂ) (psi : StateVector R) :
+    G.applyVec (c • psi) = c • G.applyVec psi :=
+  HilbertOperator.applyVec_smul (G : HilbertOperator R) c psi
+
+@[simp]
+theorem applyVec_neg (G : Gate R) (psi : StateVector R) :
+    G.applyVec (-psi) = -G.applyVec psi :=
+  HilbertOperator.applyVec_neg (G : HilbertOperator R) psi
+
+theorem apply_add (G : Gate R) (psi phi : StateVector R) :
+    G.applyVec (psi + phi) = G.applyVec psi + G.applyVec phi :=
+  applyVec_add G psi phi
+
+theorem apply_sub (G : Gate R) (psi phi : StateVector R) :
+    G.applyVec (psi - phi) = G.applyVec psi - G.applyVec phi :=
+  applyVec_sub G psi phi
+
+theorem apply_smul (G : Gate R) (c : ℂ) (psi : StateVector R) :
+    G.applyVec (c • psi) = c • G.applyVec psi :=
+  applyVec_smul G c psi
+
+theorem apply_neg (G : Gate R) (psi : StateVector R) :
+    G.applyVec (-psi) = -G.applyVec psi :=
+  applyVec_neg G psi
+
+@[simp]
+theorem one_apply (psi : PureState R) : (1 : Gate R).apply psi = psi := by
+  ext i
+  change HilbertOperator.applyVec (1 : HilbertOperator R) (psi : StateVector R) i = psi i
+  rw [HilbertOperator.one_applyVec]
+
+@[simp]
+theorem one_applyVec (psi : StateVector R) : (1 : Gate R).applyVec psi = psi :=
+  HilbertOperator.one_applyVec psi
+
+theorem mul_applyVec (G K : Gate R) (psi : StateVector R) :
+    (G * K).applyVec psi = G.applyVec (K.applyVec psi) :=
+  HilbertOperator.mul_applyVec (G : HilbertOperator R) (K : HilbertOperator R) psi
+
+/-- Applying a gate after its adjoint returns the original vector. -/
+theorem applyVec_conjTranspose_applyVec (G : Gate R) (psi : StateVector R) :
+    G.applyVec (G.conjTranspose.applyVec psi) = psi := by
+  change HilbertOperator.applyVec (G : HilbertOperator R)
+    (HilbertOperator.applyVec (G.conjTranspose : HilbertOperator R) psi) = psi
+  rw [← HilbertOperator.mul_applyVec]
+  have hGG :
+      (G : HilbertOperator R) *
+          (G.conjTranspose : HilbertOperator R) =
+        1 := by
+    change (G : HilbertOperator R) *
+          (G : HilbertOperator R).conjTranspose =
+        1
+    rw [← Matrix.star_eq_conjTranspose]
+    exact Matrix.mem_unitaryGroup_iff.mp G.unitary
+  rw [hGG, HilbertOperator.one_applyVec]
+
+/-- Applying a gate's adjoint after the gate returns the original vector. -/
+theorem conjTranspose_applyVec_applyVec (G : Gate R) (psi : StateVector R) :
+    G.conjTranspose.applyVec (G.applyVec psi) = psi := by
+  change HilbertOperator.applyVec (G.conjTranspose : HilbertOperator R)
+    (HilbertOperator.applyVec (G : HilbertOperator R) psi) = psi
+  rw [← HilbertOperator.mul_applyVec]
+  have hGG :
+      (G.conjTranspose : HilbertOperator R) *
+          (G : HilbertOperator R) =
+        1 := by
+    change (G : HilbertOperator R).conjTranspose *
+          (G : HilbertOperator R) =
+        1
+    rw [← Matrix.star_eq_conjTranspose]
+    exact Matrix.mem_unitaryGroup_iff'.mp G.unitary
+  rw [hGG, HilbertOperator.one_applyVec]
+
+theorem mul_apply (G K : Gate R) (psi : PureState R) :
+    (G * K).apply psi = G.apply (K.apply psi) := by
+  ext i
+  change (G * K).applyVec (psi : StateVector R) i
+      = G.applyVec (K.applyVec (psi : StateVector R)) i
+  rw [mul_applyVec]
+
+/-- A gate sends the basis ket `|x>` to its `x`-th column. -/
+theorem apply_ket (G : Gate R) (x : R.Index) (i : R.Index) :
+    G.apply (PureState.ket x) i = G i x := by
+  rw [apply_apply]
+  simp only [PureState.ket_apply, mul_ite, mul_one, mul_zero]
+  exact Fintype.sum_ite_eq' x (fun j => G i j)
+
+/-! ## Permutation gates -/
+
+/-- The gate permuting the computational basis by `sigma`. -/
+def ofPerm (sigma : Equiv.Perm R.Index) : Gate R :=
+  ofUnitary (sigma.permMatrix ℂ) (by
+    rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose,
+      Matrix.conjTranspose_permMatrix, ← Matrix.permMatrix_mul,
+      inv_mul_cancel, Matrix.permMatrix_one])
+
+theorem ofPerm_apply (sigma : Equiv.Perm R.Index) (psi : PureState R)
+    (i : R.Index) : (ofPerm sigma).apply psi i = psi (sigma i) := by
+  change HilbertOperator.applyVec (sigma.permMatrix ℂ) (psi : StateVector R) i =
+    psi (sigma i)
+  unfold HilbertOperator.applyVec
+  rw [Matrix.permMatrix_mulVec]
+  rfl
+
+theorem ofPerm_apply_ket (sigma : Equiv.Perm R.Index) (x : R.Index) :
+    (ofPerm sigma).apply (PureState.ket x) = PureState.ket (sigma⁻¹ x) := by
+  ext i
+  rw [ofPerm_apply, PureState.ket_apply, PureState.ket_apply]
+  by_cases h : sigma i = x
+  · rw [if_pos h, if_pos (by rw [← h]; exact (Equiv.symm_apply_apply sigma i).symm)]
+  · rw [if_neg h,
+      if_neg (fun hi => h (by rw [hi]; exact Equiv.apply_symm_apply sigma x))]
+
+theorem ofPerm_mem_unitaryGroup (sigma : Equiv.Perm R.Index) :
+    (ofPerm sigma : HilbertOperator R) ∈ Matrix.unitaryGroup R.Index ℂ :=
+  (ofPerm sigma).unitary
+
+/-! ## Unitary gates preserve inner products and norms -/
+
+/-- Unitary gates preserve the inner product. -/
+theorem inner_apply_apply_of_mem_unitaryGroup {U : Gate R}
+    (_hU : (U : HilbertOperator R) ∈ Matrix.unitaryGroup R.Index ℂ)
+    (psi phi : PureState R) :
+    inner ℂ (U.apply psi : StateVector R) (U.apply phi : StateVector R)
+      = inner ℂ (psi : StateVector R) (phi : StateVector R) :=
+  HilbertOperator.inner_applyVec_applyVec_of_mem_unitaryGroup U.unitary
+    (psi : StateVector R) (phi : StateVector R)
+
+/-- Unitary gates preserve the norm. -/
+theorem norm_apply_of_mem_unitaryGroup {U : Gate R}
+    (_hU : (U : HilbertOperator R) ∈ Matrix.unitaryGroup R.Index ℂ)
+    (psi : PureState R) :
+    ‖(U.apply psi : StateVector R)‖ = ‖(psi : StateVector R)‖ :=
+  HilbertOperator.norm_applyVec_of_mem_unitaryGroup U.unitary (psi : StateVector R)
+
+theorem norm_apply (U : Gate R) (psi : PureState R) :
+    ‖(U.apply psi : StateVector R)‖ = 1 :=
+  (U.apply psi).norm_eq_one
+
+end
+
+end Gate
+
+end Cslib.Quantum
diff --git a/Cslib/Computability/Quantum/Register.lean b/Cslib/Computability/Quantum/Register.lean
new file mode 100644
index 000000000..ed98e59f9
--- /dev/null
+++ b/Cslib/Computability/Quantum/Register.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 QudeLeap. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: QudeLeap Team
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.Fintype.Prod
+
+/-!
+# Finite quantum registers
+
+`Register` is the finite-dimensional basis interface shared by states, gates,
+operators, measurements, and circuits.  `Qubits n` is the specialization whose
+basis labels are the current big-endian `Fin (2^n)` computational basis.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+/-- A finite-dimensional quantum register. -/
+structure Register where
+  /-- Basis labels for the register. -/
+  Index : Type
+  /-- The basis is finite. -/
+  fintype : Fintype Index
+  /-- Basis labels have decidable equality. -/
+  decEq : DecidableEq Index
+
+attribute [instance] Register.fintype Register.decEq
+
+namespace Register
+
+/-- Product/tensor register. -/
+def prod (left right : Register) : Register := by
+  letI : Fintype left.Index := left.fintype
+  letI : DecidableEq left.Index := left.decEq
+  letI : Fintype right.Index := right.fintype
+  letI : DecidableEq right.Index := right.decEq
+  exact
+    { Index := left.Index × right.Index
+      fintype := inferInstance
+      decEq := inferInstance }
+
+end Register
+
+/-- The `n`-qubit register with big-endian computational basis labels. -/
+abbrev Qubits (n : Nat) : Register where
+  Index := Fin (2 ^ n)
+  fintype := inferInstance
+  decEq := inferInstance
+
+end Cslib.Quantum
diff --git a/Cslib/Computability/Quantum/State.lean b/Cslib/Computability/Quantum/State.lean
new file mode 100644
index 000000000..1acd4d1d0
--- /dev/null
+++ b/Cslib/Computability/Quantum/State.lean
@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2026 QudeLeap. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: QudeLeap Team
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Computability.Quantum.Register
+public import Mathlib.Analysis.InnerProductSpace.PiL2
+
+/-!
+# Pure states over finite registers
+
+`StateVector R` is the raw Hilbert-space vector type over a finite register
+`R`.  `PureState R` bundles a raw vector with a unit-norm proof.
+
+The qubit specialization is written `StateVector (Qubits n)` and
+`PureState (Qubits n)`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Quantum
+
+/-- Raw Hilbert-space vector for a finite quantum register. -/
+abbrev StateVector (R : Register) : Type := EuclideanSpace ℂ R.Index
+
+/-- A pure state: a unit vector in the computational Hilbert space. -/
+structure PureState (R : Register) where
+  /-- Underlying Hilbert-space vector. -/
+  vec : StateVector R
+  /-- Pure states are normalized by definition. -/
+  norm_eq_one : ‖vec‖ = 1
+
+namespace PureState
+
+noncomputable section
+
+variable {R : Register}
+
+instance : Coe (PureState R) (StateVector R) := ⟨PureState.vec⟩
+instance : CoeTail (PureState R) (StateVector R) := ⟨PureState.vec⟩
+instance : CoeOut (PureState R) (StateVector R) := ⟨PureState.vec⟩
+
+instance : CoeFun (PureState R) (fun _ => R.Index → ℂ) :=
+  ⟨fun psi => psi.vec⟩
+
+instance : Norm (PureState R) := ⟨fun psi => ‖(psi : StateVector R)‖⟩
+
+instance : Inner ℂ (PureState R) :=
+  ⟨fun psi phi => inner ℂ (psi : StateVector R) (phi : StateVector R)⟩
+
+instance : HAdd (PureState R) (PureState R) (StateVector R) :=
+  ⟨fun psi phi => (psi : StateVector R) + (phi : StateVector R)⟩
+
+instance : HSub (PureState R) (PureState R) (StateVector R) :=
+  ⟨fun psi phi => (psi : StateVector R) - (phi : StateVector R)⟩
+
+instance : HSMul ℂ (PureState R) (StateVector R) :=
+  ⟨fun c psi => c • (psi : StateVector R)⟩
+
+@[simp]
+theorem hAdd_apply (psi phi : PureState R) (i : R.Index) :
+    (psi + phi : StateVector R) i = psi i + phi i := rfl
+
+@[simp]
+theorem hSub_apply (psi phi : PureState R) (i : R.Index) :
+    (psi - phi : StateVector R) i = psi i - phi i := rfl
+
+@[simp]
+theorem hSMul_apply (c : ℂ) (psi : PureState R) (i : R.Index) :
+    (c • psi : StateVector R) i = c * psi i := rfl
+
+/-- Build a pure state from a normalized Hilbert-space vector. -/
+def ofVec (v : StateVector R) (h : ‖v‖ = 1) : PureState R := ⟨v, h⟩
+
+@[simp]
+theorem coe_ofVec (v : StateVector R) (h : ‖v‖ = 1) :
+    ((ofVec v h : PureState R) : StateVector R) = v := rfl
+
+@[simp]
+theorem ofVec_apply (v : StateVector R) (h : ‖v‖ = 1) (i : R.Index) :
+    ofVec v h i = v i := rfl
+
+@[simp]
+theorem norm_eq_one' (psi : PureState R) : ‖(psi : StateVector R)‖ = 1 :=
+  psi.norm_eq_one
+
+@[ext]
+theorem ext {psi phi : PureState R} (h : ∀ i, psi i = phi i) : psi = phi := by
+  cases psi with
+  | mk psi hpsi =>
+    cases phi with
+    | mk phi hphi =>
+      have hv : psi = phi := by
+        apply WithLp.ofLp_injective
+        funext i
+        exact h i
+      subst hv
+      rfl
+
+/-- Computational-basis ket over a finite register. -/
+def ket (x : R.Index) : PureState R :=
+  ofVec (PiLp.single 2 x 1) (by simp)
+
+@[simp]
+theorem ket_apply (x i : R.Index) : ket x i = if i = x then 1 else 0 := by
+  simp [ket]
+
+theorem ket_injective : Function.Injective (ket (R := R)) := by
+  intro x y hxy
+  by_contra hne
+  have h : ket x x = ket y x := by rw [hxy]
+  rw [ket_apply, ket_apply, if_pos rfl, if_neg hne] at h
+  exact one_ne_zero h
+
+theorem norm_ket (x : R.Index) : ‖(ket x : StateVector R)‖ = 1 :=
+  (ket x).norm_eq_one
+
+end
+
+end PureState
+
+end Cslib.Quantum
diff --git a/CslibTests.lean b/CslibTests.lean
index 3380bb5e1..39303e992 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -10,4 +10,5 @@ import CslibTests.ImportWithMathlib
 import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
+import CslibTests.Quantum
 import CslibTests.Reduction
diff --git a/CslibTests/Quantum.lean b/CslibTests/Quantum.lean
new file mode 100644
index 000000000..fa8c28c3d
--- /dev/null
+++ b/CslibTests/Quantum.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 QudeLeap. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: QudeLeap Team
+-/
+
+import Cslib.Computability.Quantum.Gate
+
+namespace CslibTests
+
+open Cslib.Quantum
+
+/-! # Quantum computing foundation smoke tests -/
+
+example : (Qubits 2).Index = Fin 4 := rfl
+
+example (x : (Qubits 2).Index) : PureState.ket x x = 1 := by
+  simp
+
+example {x y : (Qubits 2).Index} (h : PureState.ket x = PureState.ket y) : x = y :=
+  PureState.ket_injective h
+
+example (A : HilbertOperator (Qubits 1)) (x i : (Qubits 1).Index) :
+    HilbertOperator.applyVec A (PureState.ket x : StateVector (Qubits 1)) i = A i x := by
+  simp
+
+example (ψ : PureState (Qubits 1)) : (1 : Gate (Qubits 1)).apply ψ = ψ := by
+  simp
+
+example (G K : Gate (Qubits 1)) (ψ : PureState (Qubits 1)) :
+    (G * K).apply ψ = G.apply (K.apply ψ) :=
+  Gate.mul_apply G K ψ
+
+example (U : Gate (Qubits 1)) (ψ φ : PureState (Qubits 1)) :
+    inner ℂ (U.apply ψ : StateVector (Qubits 1)) (U.apply φ : StateVector (Qubits 1)) =
+      inner ℂ (ψ : StateVector (Qubits 1)) (φ : StateVector (Qubits 1)) :=
+  Gate.inner_apply_apply_of_mem_unitaryGroup (U := U) U.unitary ψ φ
+
+example (U : Gate (Qubits 1)) (ψ : PureState (Qubits 1)) :
+    ‖(U.apply ψ : StateVector (Qubits 1))‖ = 1 :=
+  Gate.norm_apply U ψ
+
+/-- The one-qubit bit-flip permutation. -/
+def bitFlip : Equiv.Perm (Qubits 1).Index :=
+  Equiv.swap (0 : Fin 2) (1 : Fin 2)
+
+example (ψ : PureState (Qubits 1)) (i : (Qubits 1).Index) :
+    (Gate.ofPerm bitFlip).apply ψ i = ψ (bitFlip i) := by
+  simpa using Gate.ofPerm_apply bitFlip ψ i
+
+example :
+    (Gate.ofPerm bitFlip).apply (PureState.ket (0 : Fin 2)) = PureState.ket (1 : Fin 2) := by
+  rw [Gate.ofPerm_apply_ket]
+  ext i
+  fin_cases i <;> rfl
+
+/-! A direct Bell-state example, before tensor products and named gates are introduced. -/
+
+/-- The Bell state `(∣00⟩ + ∣11⟩) / √2`, represented directly in the two-qubit basis. -/
+noncomputable def bell00Vec : StateVector (Qubits 2) :=
+  WithLp.toLp 2 ![(Real.sqrt 2 : ℂ)⁻¹, 0, 0, (Real.sqrt 2 : ℂ)⁻¹]
+
+theorem bell00Vec_norm : ‖bell00Vec‖ = 1 := by
+  rw [EuclideanSpace.norm_eq]
+  simp [bell00Vec, Fin.sum_univ_four, Real.sq_sqrt]
+  norm_num
+
+/-- The Bell state `(∣00⟩ + ∣11⟩) / √2` as a pure state. -/
+noncomputable def bell00 : PureState (Qubits 2) :=
+  PureState.ofVec bell00Vec bell00Vec_norm
+
+example : bell00 (0 : Fin 4) = (Real.sqrt 2 : ℂ)⁻¹ := rfl
+example : bell00 (1 : Fin 4) = 0 := rfl
+example : bell00 (2 : Fin 4) = 0 := rfl
+example : bell00 (3 : Fin 4) = (Real.sqrt 2 : ℂ)⁻¹ := rfl
+
+example : ‖(bell00 : StateVector (Qubits 2))‖ = 1 :=
+  bell00.norm_eq_one
+
+example : (1 : Gate (Qubits 2)).apply bell00 = bell00 := by
+  simp
+
+end CslibTests