OAI/Computability/QuantumFactoring/OracleReadOnly.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.Instruction.target_reverse line 18
2. lemma OAI.ExactQuantumFactoring.Instruction.target_place line 19
3. lemma OAI.ExactQuantumFactoring.notAt_target line 21
4. lemma OAI.ExactQuantumFactoring.cnotAt_target line 22
5. lemma OAI.ExactQuantumFactoring.toffoliAt_target line 23
6. lemma OAI.ExactQuantumFactoring.BooleanOp.compile_target line 26
7. lemma OAI.ExactQuantumFactoring.BooleanProgram.compile_target line 34
8. lemma OAI.ExactQuantumFactoring.BoolNet.program_target line 41
9. lemma OAI.ExactQuantumFactoring.BooleanNetwork.copyPrefix_target line 53
10. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracle_target line 65
11. lemma OAI.ExactQuantumFactoring.BooleanNetwork.oracleOn_target line 79

    Source documentation

    Compute/copy/uncompute never targets a read-only input, including on malformed scratch states. This global property is what reflection needs.

    lemma BooleanNetwork.oracleOn_target {n m r : ℕ} (c : BooleanNetwork n m) (hr : c.net.count≤r) :
        ∀ o∈oracleOn c hr,n≤o.target.val := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.BooleanNetwork.oracleOn

12. lemma OAI.ExactQuantumFactoring.targetProgram_target line 88
13. lemma OAI.ExactQuantumFactoring.preparedOracle_target line 95
14. lemma OAI.ExactQuantumFactoring.preparedOracle_readOnly line 104

    Source documentation

    The bit prefix is preserved for every input sector, without any data correctness or clean-work premise.

    lemma preparedOracle_readOnly {n m r : ℕ} (c : BooleanNetwork n m) (hr : c.net.count≤r)
        (P : List (Instruction m)) :
        ReadOnly (Finset.univ.filter (fun i : Fin (n+m+r)=>i.val<n)) (preparedOracle c hr P) := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.ReadOnly, OAI.ExactQuantumFactoring.preparedOracle