OAI/Computability/QuantumFactoring/RetrospectiveStatistics.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.recordPhi line 22

   Source documentation

   The closed statistics are evaluated over the supplied exponent record, not by enumerating residues or invoking a factorization oracle.

   noncomputable def recordPhi (f : FactorRecord) : ℕ :=
   …

   Mentions: OAI.ExactQuantumFactoring.FactorRecord

2. def OAI.ExactQuantumFactoring.recordFavorable line 25
3. lemma OAI.ExactQuantumFactoring.recordPhi_factorization line 29
4. lemma OAI.ExactQuantumFactoring.recordFavorable_factorization line 35
5. def OAI.ExactQuantumFactoring.dataRecord line 43
6. lemma OAI.ExactQuantumFactoring.dataRecord_correct line 46
7. def OAI.ExactQuantumFactoring.dataPhi line 51
8. def OAI.ExactQuantumFactoring.dataFavorable line 52
9. lemma OAI.ExactQuantumFactoring.dataPhi_correct line 54
10. lemma OAI.ExactQuantumFactoring.dataFavorable_correct line 58
11. def OAI.ExactQuantumFactoring.stripFactorsNat line 64

    Source documentation

    Literal prime stripping in natural modular arithmetic. This is exactly the scan compiled by stripScan; its inputs come only from the supplied data.

    def stripFactorsNat (a m : ℕ) : List ℕ→ℕ→ℕ
      | [], v => v
      | q::qs, v => stripFactorsNat a m qs (stripPrimeNat a m q v)

    Mentions: OAI.ExactQuantumFactoring.stripPrimeNat

12. lemma OAI.ExactQuantumFactoring.stripFactorsNat_unit line 68
13. def OAI.ExactQuantumFactoring.dataOrder line 75
14. lemma OAI.ExactQuantumFactoring.dataOrder_correct line 80

    Source documentation

    The retrospective order used for EVERY actual requested cofactor is the true order, without calling an order oracle during execution.

    lemma dataOrder_correct {M m a : ℕ} (hM : 0 < M) (hm : 2 ≤ m) (hd : m∣M)
        (u : (ZMod m)ˣ) (ha : (a : ZMod m)=(u : ZMod m)) :
        dataOrder (trueData M) a m=orderOf u := by
    …

    Mentions: OAI.ExactQuantumFactoring.dataOrder, OAI.ExactQuantumFactoring.trueData

15. def OAI.ExactQuantumFactoring.dataListSuccess line 87
16. def OAI.ExactQuantumFactoring.dataOrderSuccess line 89
17. lemma OAI.ExactQuantumFactoring.dataListSuccess_correct line 92
18. lemma OAI.ExactQuantumFactoring.dataOrderSuccess_correct line 97