OAI/Computability/QuantumFactoring/FactorEncoding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PaddedOrder line 14

   Source documentation

   Zero padding follows every positive entry.

   def PaddedOrder (a b : ℕ) : Prop := b=0 ∨ (a≠0 ∧ a≤b)

2. def OAI.ExactQuantumFactoring.unpadProduct line 16
3. def OAI.ExactQuantumFactoring.FactorListValid line 18
4. lemma OAI.ExactQuantumFactoring.paddedOrder_append line 21
5. lemma OAI.ExactQuantumFactoring.unpadProduct_append line 33
6. lemma OAI.ExactQuantumFactoring.FactorListValid.decompose line 42
7. lemma OAI.ExactQuantumFactoring.factorListValid_iff line 83
8. lemma OAI.ExactQuantumFactoring.correctEncoding_unique line 96
9. theorem OAI.ExactQuantumFactoring.correctEncoding_exists line 107

   Source documentation

   The valid sorted padded encoding exists and is unique, with every entry in its n-bit range; the mathematical factor list here is used for analysis only.

   theorem correctEncoding_exists {N n : ℕ} (hN : 2≤N) (hb : N<2^n) :
       ∃ xs : List ℕ, CorrectEncoding N n xs ∧ xs.length=n ∧ ∀ a ∈ xs, a<2^n := by
   …

   Mentions: OAI.ExactQuantumFactoring.CorrectEncoding