OAI/Computability/QuantumFactoring/TransitionWords.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.TransitionWords.encode line 24

    Source documentation

    K n-bit words in consecutive little-endian fields, followed by one zero word. This fits exactly the source's W=n(K+1) output cap.

    def encode {n K : ℕ} (a : Fin K→Basis n) : Basis (n*(K+1)) := fun i =>
…

    Mentions: OAI.ExactQuantumFactoring.Basis

  2. def OAI.ExactQuantumFactoring.TransitionWords.read line 28
  3. lemma OAI.ExactQuantumFactoring.TransitionWords.read_encode line 31
  4. lemma OAI.ExactQuantumFactoring.TransitionWords.encode_injective line 36
  5. lemma OAI.ExactQuantumFactoring.TransitionWords.pow_width_le line 42
  6. abbrev OAI.ExactQuantumFactoring.ListSlots.K line 50
  7. abbrev OAI.ExactQuantumFactoring.ListSlots.Ordinary line 51
  8. abbrev OAI.ExactQuantumFactoring.ListSlots.Result line 52
  9. def OAI.ExactQuantumFactoring.ListSlots.fresh line 55
  10. def OAI.ExactQuantumFactoring.ListSlots.ordinary line 59
  11. def OAI.ExactQuantumFactoring.ListSlots.canonical line 62
  12. def OAI.ExactQuantumFactoring.ListSlots.passed line 65
  13. def OAI.ExactQuantumFactoring.ListSlots.output line 69
  14. def OAI.ExactQuantumFactoring.ListSlots.GoodOutput line 72
  15. lemma OAI.ExactQuantumFactoring.ListSlots.ordinary_good line 77
  16. lemma OAI.ExactQuantumFactoring.ListSlots.canonical_good line 86
  17. lemma OAI.ExactQuantumFactoring.ListSlots.fresh_normalized line 91
  18. lemma OAI.ExactQuantumFactoring.ListSlots.passed_mass line 94
  19. lemma OAI.ExactQuantumFactoring.ListSlots.passed_good line 99