OAI/Computability/QuantumFactoring/DyadicCompletion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.Completion.coeff line 18
  2. def OAI.ExactQuantumFactoring.Completion.guessRetention line 19
  3. def OAI.ExactQuantumFactoring.Completion.coinBits line 21
  4. lemma OAI.ExactQuantumFactoring.Completion.coeff_at line 23
  5. lemma OAI.ExactQuantumFactoring.Completion.guess_at line 28
  6. abbrev OAI.ExactQuantumFactoring.Completion.Raw line 44
  7. def OAI.ExactQuantumFactoring.Completion.fresh line 45
  8. def OAI.ExactQuantumFactoring.Completion.rare line 49
  9. instance OAI.ExactQuantumFactoring.Completion.(instance at line 50) line 50
  10. def OAI.ExactQuantumFactoring.Completion.threshold line 53
  11. def OAI.ExactQuantumFactoring.Completion.output line 56
  12. def OAI.ExactQuantumFactoring.Completion.ordinaryPass line 59
  13. def OAI.ExactQuantumFactoring.Completion.guessPass line 61
  14. def OAI.ExactQuantumFactoring.Completion.passed line 63
  15. lemma OAI.ExactQuantumFactoring.Completion.fair_eq_mass line 66
  16. lemma OAI.ExactQuantumFactoring.Completion.fresh_normalized line 71
  17. theorem OAI.ExactQuantumFactoring.Completion.passed_mass line 83

    Source documentation

    Actual fresh registers do NOT depend on s, goodness or the canonical output. Those values are used only by the later classical test on the retained record.

    theorem passed_mass {α : Type*} [Fintype α] {W t d j : ℕ}
    (ψ : α→ℂ) (good : α→Prop) (y₀ : Basis W) (s z : ℚ)
    (hψ : ∑ x,Complex.normSq (ψ x)=1) (hgood : outcomeMass good ψ=(s:ℝ))
    (hsd : DyadicAt d s) (hzd : DyadicAt j z) (hj : j≤coinBits W t d)
    (hs₀ : 0<s) (hs₁ : s≤1) (ht : 0<t) (hz : 0<z)
    (hzA : z≤(1-1/(2:ℚ)^t)*s) :
    outcomeMass (passed good y₀ s z) (fresh ψ W t d)=(z:ℝ) := by
…

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.coinBits, OAI.ExactQuantumFactoring.Completion.passed, OAI.ExactQuantumFactoring.Completion.fresh

  18. lemma OAI.ExactQuantumFactoring.Completion.passed_good line 132
  19. def OAI.ExactQuantumFactoring.Completion.program line 141

    Source documentation

    Literal fixed-gate program for the raw extended record; no oracle for the future data, success probability, or distinguished guess occurs in its code.

    def program {q : ℕ} (P : List (Instruction q)) (W t d : ℕ) :
    List (Instruction (t+(q+(W+coinBits W t d)))) :=
…

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Completion.coinBits

  20. def OAI.ExactQuantumFactoring.Completion.layout line 145
  21. lemma OAI.ExactQuantumFactoring.Completion.program_entry line 147
  22. lemma OAI.ExactQuantumFactoring.Completion.program_length line 154