OAI/Computability/QuantumFactoring/SamplerDecodeCircuit.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BooleanNetwork.leftNet line 18
2. def OAI.ExactQuantumFactoring.BooleanNetwork.rightNet line 19
3. lemma OAI.ExactQuantumFactoring.BooleanNetwork.leftNet_eval line 20
4. lemma OAI.ExactQuantumFactoring.BooleanNetwork.rightNet_eval line 24
5. lemma OAI.ExactQuantumFactoring.BooleanNetwork.equalOn_basis line 28
6. def OAI.ExactQuantumFactoring.OrderTrial.sampleYNet line 39
7. def OAI.ExactQuantumFactoring.OrderTrial.sampleUNet line 41
8. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleYNet_eval line 43
9. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleUNet_eval line 45
10. def OAI.ExactQuantumFactoring.OrderTrial.triangularSelectedNet line 48
11. lemma OAI.ExactQuantumFactoring.OrderTrial.triangularSelectedNet_eval line 50
12. def OAI.ExactQuantumFactoring.OrderTrial.samplerSelectedNet line 58

    Source documentation

    Full selection compares retained read-only inputs and every sampler scratch bit, not only the apparent phase and modular residue fields.

    def samplerSelectedNet {k u b : ℕ} (a m : BooleanNetwork k u)
        (z : BooleanNetwork k (OrderSample.width u b)) : BooleanNetwork k 1 :=
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderSample.width

13. lemma OAI.ExactQuantumFactoring.OrderTrial.samplerSelectedNet_eval line 63
14. lemma OAI.ExactQuantumFactoring.OrderTrial.samplerSelectedNet_count line 69