readme

Author: goliath-klein

README.md

@@ -11,15 +11,15 @@ gates and quantum circuits.
 * `QCLib/Mathlib`
 
 This directory contains results that are of sufficient generality that they
-might be of interest to Mathlib. There is no implication that the results are
-already sufficiently polished to be upstreamed.
+might be of interest to Mathlib. (There is no implication that the results are
+already sufficiently polished to be upstreamed).
 
 * `QCLib/Mathlib/PiOuterProduct.lean`
   `QCLib/Mathlib/UnitaryGroup/PiKronecker.lean`
 
 The files define tensor products of indexed families of concrete vectors (i.e.
 functions into a `CommMonoid`) and of (unitary) matrices. Most of the rest of the library
-builds on these definitions.
+builds on these definitions. This is the most mature part of the library at the moment.
 
 * `QCLib/Mathlib/UnitaryGroup/Lemmas.lean` 
   `QCLib/Matrix/UnitaryGroup`
@@ -39,23 +39,24 @@ Permutations and controlled gates. Not restricted to qubits.
 * `QCLib/Circuit/Gate/Qubit/Embed.lean`
 
 The embedding of single-party and bipartite unitaries into the unitary group on
-a tensor product. Most results are dependently-typed (i.e. working for inhomogeneous factors).
+a tensor product. Most results are dependently-typed (i.e. they work for tensor
+products with inhomogeneous factors).
 
 * `QCLib/Circuit/Gate/Qubit/PauliGroup`
 
 Some basic results on the `n`-qubit Pauli group.
 
 * `QCLib/Circuit/Gate/Qubit/QFT.lean`
 
-A first implementation of a QFT circuit. [This is still quite messy. Cleanup is ongoing.]
+A first implementation of a QFT circuit. [Cleanup is ongoing.]
 
 * `QCLib/Circuit/Gate/Qubit/CZ.lean`
 
 Work towards the "diagonal real Clifford group", i.e. the group generated by `Z` and controlled-`Z` gates. Goal is to reason about graph states. Incomplete.
 
 * `QCLib/Circuit/Gate/Qubit/Complexity.lean`
 
-Experiment for defining the gate complexity of a unitary. (Other projects seem to have much more sophisticated frameworks for talking about the syntax of quantum circuits / algorithms. So this might be a dead end).
+Experiment for defining the gate complexity of a unitary. (Other projects seem to have much more sophisticated frameworks for talking about the syntax of quantum circuits / algorithms. So this file might be a dead end).
 
 * `QCLib/Tactic/MatrixExpand.lean`