OAI/Computability/QuantumFactoring/OracleLayout.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.BooleanNetwork.packed line 15

    Source documentation

    Input, output, then zero work space; this same layout is used by the classical subroutines inside the coherent controller.

    def packed {n m : ℕ} (r : ℕ) (x : Basis n) (y : Basis m) : Basis (n+m+r) :=
…

    Mentions: OAI.ExactQuantumFactoring.Basis

  2. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_input line 19
  3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_target line 22
  4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.packed_work line 25
  5. def OAI.ExactQuantumFactoring.BooleanNetwork.oracleIndex line 29
  6. def OAI.ExactQuantumFactoring.BooleanNetwork.oraclePlacement line 34

    Source documentation

    Place the oracle's retained trace after its output rather than between the input and output. A larger reservoir of work wires is permitted.

    def oraclePlacement {n m r : ℕ} (c : BooleanNetwork n m) (hr : c.net.count ≤ r) :
    Register (c.width+m) (n+m+r) where
…

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Register

  7. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oraclePlacement_val line 50
  8. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oraclePlacement_input line 54
  9. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oraclePlacement_target line 61
  10. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oraclePlacement_work line 68
  11. def OAI.ExactQuantumFactoring.BooleanNetwork.oracleOn line 75
  12. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracleOn_length line 78
  13. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracleOn_basis line 82