OAI/Computability/QuantumFactoring/RetrospectiveCircuit.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.stripPrimeNat line 18
2. lemma OAI.ExactQuantumFactoring.stripPrimeNat_unit line 21
3. def OAI.ExactQuantumFactoring.BitArithmetic.liftInput line 39
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.liftInput_eval line 42
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.liftInput_count line 45
6. def OAI.ExactQuantumFactoring.BitArithmetic.powOn line 48
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.powOn_value line 51
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.powOn_count line 62
9. def OAI.ExactQuantumFactoring.BitArithmetic.stripOn line 69
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripOn_value line 75
11. def OAI.ExactQuantumFactoring.BitArithmetic.stripStepBound line 98
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripOn_count line 100
13. def OAI.ExactQuantumFactoring.BitArithmetic.stripUpdate line 114

    Source documentation

    The original input stays read-only; the accumulator is updated once.

    def stripUpdate {k w : ℕ} (a m q : BooleanNetwork k w) : BooleanNetwork (k+w) (k+w) :=
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

14. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripUpdate_value line 118
15. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripUpdate_count line 135
16. def OAI.ExactQuantumFactoring.BitArithmetic.stripScan line 141
17. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripScan_count line 145
18. lemma OAI.ExactQuantumFactoring.BitArithmetic.stripScan_unit line 156
19. theorem OAI.ExactQuantumFactoring.BitArithmetic.stripScan_exact line 174

    Source documentation

    Exact order from the completed data, by explicit polynomial-size Boolean networks of division and repeated modular squaring.

    theorem stripScan_exact {k w m : ℕ} (hm : 2 ≤ m) (aN mN : BooleanNetwork k w)
        (u : (ZMod m)ˣ) (qs : List (BooleanNetwork k w)) (x : Basis k) (z : Basis w)
        (ha : ((bitsValue (aN.eval x)).toNat : ZMod m)=(u : ZMod m))
        (hmN : (bitsValue (mN.eval x)).toNat=m) (hz : (bitsValue z).toNat=m.totient)
        (hp : ∀ q∈qs, ((bitsValue (q.eval x)).toNat).Prime)
        (hprod : (qs.map (fun q => (bitsValue (q.eval x)).toNat)).prod=m.totient) :
        ∃ z', (stripScan aN mN qs).eval (Fin.append x z)=Fin.append x z' ∧ (bitsValue z').toNat=orderOf u := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.stripScan