OAI/Computability/QuantumFactoring/OrderSampleCircuit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Actual modular-power/triangular-transform order sampler. All arithmetic inputs are read-only wires; the modular output remains coherent.

  1. abbrev OAI.ExactQuantumFactoring.OrderSample.inputWidth line 20
  2. def OAI.ExactQuantumFactoring.OrderSample.inputWord line 22
  3. def OAI.ExactQuantumFactoring.OrderSample.powerInputs line 25
  4. lemma OAI.ExactQuantumFactoring.OrderSample.powerInputs_eval line 29
  5. def OAI.ExactQuantumFactoring.OrderSample.powerNetwork line 38
  6. lemma OAI.ExactQuantumFactoring.OrderSample.powerNetwork_count line 41
  7. lemma OAI.ExactQuantumFactoring.OrderSample.powerNetwork_value line 46
  8. lemma OAI.ExactQuantumFactoring.OrderSample.powerNetwork_eq line 53
  9. abbrev OAI.ExactQuantumFactoring.OrderSample.scratch line 63
  10. abbrev OAI.ExactQuantumFactoring.OrderSample.width line 64
  11. def OAI.ExactQuantumFactoring.OrderSample.program line 66
  12. lemma OAI.ExactQuantumFactoring.OrderSample.program_length line 70
  13. def OAI.ExactQuantumFactoring.OrderSample.word line 81
  14. def OAI.ExactQuantumFactoring.OrderSample.uniformInput line 84
  15. lemma OAI.ExactQuantumFactoring.OrderSample.transform_entry line 88
  16. lemma OAI.ExactQuantumFactoring.OrderSample.program_amplitude line 98

    Source documentation

    The physically produced selected amplitude, expressed as a finite word sum.

    lemma program_amplitude {w s : ℕ} (a m : Basis w) (y : Basis (s+2)) (u : Basis w)
    (hm : 2 ≤ (bitsValue m).toNat) :
    (programMatrix (program w s)).mulVec (uniformInput w (s+2) a m) (word a m y u) =
      ((2:ℂ)^(s+2))⁻¹ * ∑ x : Basis (s+2),
        if (bitsValue a).toNat^inputNumber x % (bitsValue m).toNat=(bitsValue u).toNat
        then OrderTrial.phase ((inputNumber x:ℝ)*outputNumber y/(2:ℝ)^(s+2)) else 0 := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderSample.program, OAI.ExactQuantumFactoring.OrderSample.uniformInput, OAI.ExactQuantumFactoring.OrderSample.word, OAI.ExactQuantumFactoring.OrderTrial.phase

  17. lemma OAI.ExactQuantumFactoring.OrderSample.inputNumber_sum line 122
  18. theorem OAI.ExactQuantumFactoring.OrderSample.program_amplitude_range line 129

    Source documentation

    Exactly 1/Q times the coherent modular-power residue sum of Section3.

    theorem program_amplitude_range {w s : ℕ} (a m : Basis w) (y : Basis (s+2)) (u : Basis w)
    (hm : 2 ≤ (bitsValue m).toNat) :
    (programMatrix (program w s)).mulVec (uniformInput w (s+2) a m) (word a m y u) =
      ((2^(s+2):ℕ):ℂ)⁻¹ * ∑ x ∈ Finset.range (2^(s+2)),
        if (bitsValue a).toNat^x % (bitsValue m).toNat=(bitsValue u).toNat
        then OrderTrial.phase ((outputNumber y:ℝ)*x/(2^(s+2):ℕ)) else 0 := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderSample.program, OAI.ExactQuantumFactoring.OrderSample.uniformInput, OAI.ExactQuantumFactoring.OrderSample.word, OAI.ExactQuantumFactoring.OrderTrial.phase