OAI/Computability/QuantumFactoring/UniversalSplit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ExactQuantumFactoring.UniversalSplit.Raw line 21

    Source documentation

    The unchanging request register dimensions depend only on the original n.

    abbrev Raw := FixedSplit.Raw

    Mentions: OAI.ExactQuantumFactoring.FixedSplit.Raw

  2. def OAI.ExactQuantumFactoring.UniversalSplit.Hard line 23
  3. def OAI.ExactQuantumFactoring.UniversalSplit.firstComponent line 27

    Source documentation

    Source's distinguished component: the least prime divisor, not an arbitrary component for which the compiler would need extra advice.

    def firstComponent {m : ℕ} (hm : 2 ≤ m) : Component m :=
…

    Mentions: OAI.ExactQuantumFactoring.Component

  4. lemma OAI.ExactQuantumFactoring.UniversalSplit.secondComponent line 30
  5. def OAI.ExactQuantumFactoring.UniversalSplit.dummyList line 38
  6. def OAI.ExactQuantumFactoring.UniversalSplit.dummyOrder line 40
  7. def OAI.ExactQuantumFactoring.UniversalSplit.dummy line 42
  8. lemma OAI.ExactQuantumFactoring.UniversalSplit.dummy_mass line 44
  9. def OAI.ExactQuantumFactoring.UniversalSplit.passed line 70
  10. lemma OAI.ExactQuantumFactoring.UniversalSplit.passed_mass line 75
  11. lemma OAI.ExactQuantumFactoring.UniversalSplit.passed_divisor line 84
  12. def OAI.ExactQuantumFactoring.UniversalSplit.fresh line 100

    Source documentation

    Every quantum preparation below is the same physical fixed-width program (on the runtime input word). Hard/easy tests affect the deferred predicate only.

    noncomputable def fresh (n m : ℕ) : Raw n→ℂ := FixedSplit.fresh (natBasis n m)

    Mentions: OAI.ExactQuantumFactoring.UniversalSplit.Raw, OAI.ExactQuantumFactoring.FixedSplit.fresh

  13. def OAI.ExactQuantumFactoring.UniversalSplit.good line 101
  14. def OAI.ExactQuantumFactoring.UniversalSplit.decode line 102
  15. lemma OAI.ExactQuantumFactoring.UniversalSplit.fresh_normalized line 104
  16. lemma OAI.ExactQuantumFactoring.UniversalSplit.good_mass line 106
  17. lemma OAI.ExactQuantumFactoring.UniversalSplit.good_divisor line 109