OAI/Computability/QuantumFactoring/SortedEncoding.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.numbers line 16
2. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.zero_number line 18
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.numbers_pad line 26
4. theorem OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort_correct line 32

   Source documentation

   Literal compare-exchange sorting gives the exact source sorted padded encoding, not just an arbitrary prime multiset.

   theorem sort_correct {w N r : ℕ} (xs : List (Basis w))
       (hp : ∀ p∈numbers xs,p.Prime) (hprod : (numbers xs).prod=N) (hlen : xs.length ≤ r) :
       CorrectEncoding N r (numbers (sort (xs++List.replicate (r-xs.length) (fun _=>false)))) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.numbers, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.BitArithmetic.SortedWords.sort