OAI/Computability/QuantumFactoring/ExactnessFurther2.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.Exactness.RespectsSector.one line 18
2. lemma OAI.ExactQuantumFactoring.Exactness.RespectsSector.mul line 24
3. def OAI.ExactQuantumFactoring.ReadOnly line 41

   Source documentation

   A syntactic read-only rule suffices; no hypothesis about the state prepared by the algorithm or its unknown factors occurs here.

   def ReadOnly {q : ℕ} (inputs : Finset (Fin q)) (P : List (Instruction q)) : Prop :=
   …

   Mentions: OAI.ExactQuantumFactoring.Instruction

4. def OAI.ExactQuantumFactoring.inputSector line 44
5. lemma OAI.ExactQuantumFactoring.Instruction.respects_input line 47
6. lemma OAI.ExactQuantumFactoring.program_respects_input line 62