OAI/Computability/QuantumFactoring/OrderTransition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.minOption line 19
2. def OAI.ExactQuantumFactoring.OrderTrial.minimumCandidate line 24
3. lemma OAI.ExactQuantumFactoring.OrderTrial.minOption_some_mem line 28
4. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumCandidate_mem line 41
5. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumCandidate_lower line 50
6. lemma OAI.ExactQuantumFactoring.OrderTrial.minOption_eq_low line 54
7. lemma OAI.ExactQuantumFactoring.OrderTrial.minimumCandidate_eq_low line 69
8. def OAI.ExactQuantumFactoring.OrderTrial.orderResult line 82

   Source documentation

   The source order transition ignores empty trials and returns the least nonempty candidate, with zero for the entirely empty list.

   noncomputable def orderResult {w : ℕ} (s n : ℕ) (a m : Basis w) (K : ℕ)
       (x : Fin K→Raw w s n) : ℕ :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderTrial.Raw

9. lemma OAI.ExactQuantumFactoring.OrderTrial.orderResult_eq_order line 86
10. theorem OAI.ExactQuantumFactoring.OrderTrial.orderResult_mass line 105

    Source documentation

    Physical repeated law (before the deterministic minimum oracle).

    theorem orderResult_mass {w n s : ℕ} (hn : 1≤n) (hs : 2^(s+2)=(2^n)^16)
        (a m : Basis w) (hm : 2≤(bitsValue m).toNat) (u : (ZMod (bitsValue m).toNat)ˣ)
        (ha : ((bitsValue a).toNat : ZMod (bitsValue m).toNat)=(u : ZMod (bitsValue m).toNat))
        (hdB : orderOf u<2^n) (K : ℕ) :
        outcomeMass (fun x => orderResult s n a m K x=orderOf u) (tensorState (rawState s n a m) K)=
          1-(1-(Nat.totient (orderOf u):ℝ)*(prescribedMass (orderOf u):ℝ))^K := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderTrial.orderResult, OAI.ExactQuantumFactoring.OrderTrial.rawState, OAI.ExactQuantumFactoring.OrderTrial.prescribedMass

11. theorem OAI.ExactQuantumFactoring.OrderTrial.orderResult_lower line 118

    Source documentation

    Original cutoff, original K=n^5, no extra oracle or changed asymptotics.

    theorem orderResult_lower {w n s : ℕ} (hn : 128≤n) (hs : 2^(s+2)=(2^n)^16)
        (a m : Basis w) (hm : 2≤(bitsValue m).toNat) (u : (ZMod (bitsValue m).toNat)ˣ)
        (ha : ((bitsValue a).toNat : ZMod (bitsValue m).toNat)=(u : ZMod (bitsValue m).toNat))
        (hdB : orderOf u<2^n) :
        1-1/(2:ℝ)^(2*n)≤outcomeMass (fun x => orderResult s n a m (n^5) x=orderOf u)
          (tensorState (rawState s n a m) (n^5)) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderTrial.orderResult, OAI.ExactQuantumFactoring.OrderTrial.rawState