OAI/Computability/QuantumFactoring/TransitionEqualization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.pow line 20
2. def OAI.ExactQuantumFactoring.Completion.target line 29
3. def OAI.ExactQuantumFactoring.Completion.transitionWidth line 30
4. def OAI.ExactQuantumFactoring.Completion.listSuccess line 31
5. def OAI.ExactQuantumFactoring.Completion.orderSuccess line 33
6. lemma OAI.ExactQuantumFactoring.Completion.target_at line 36
7. lemma OAI.ExactQuantumFactoring.Completion.listSuccess_at line 39
8. lemma OAI.ExactQuantumFactoring.Completion.orderSuccess_at line 46
9. lemma OAI.ExactQuantumFactoring.Completion.target_pos line 52
10. lemma OAI.ExactQuantumFactoring.Completion.target_le_ordinary line 60

    Source documentation

    The source repetition bound suffices for the unchanged equalization target. No high-probability event is being declared to have probability one.

    lemma target_le_ordinary {n : ℕ} (hn : 1 ≤ n) {s : ℚ}
        (hs : 1-1/(2:ℚ)^(2*n) ≤ s) :
        target n ≤ (1-1/(2:ℚ)^(2*n))*s := by
    …

    Mentions: OAI.ExactQuantumFactoring.Completion.target

11. lemma OAI.ExactQuantumFactoring.Completion.listSuccess_lower line 76
12. lemma OAI.ExactQuantumFactoring.Completion.listSuccess_le_one line 85
13. lemma OAI.ExactQuantumFactoring.Completion.orderSuccess_lower line 94
14. lemma OAI.ExactQuantumFactoring.Completion.orderSuccess_le_one line 104
15. theorem OAI.ExactQuantumFactoring.Completion.list_passed_mass line 118

    Source documentation

    Local same-record equalization, now specialized to the actual list law and actual source constants. The guess is tested for a single fixed padded list.

    theorem list_passed_mass {m n : ℕ} (hn : 128 ≤ n) (hm : 2 ≤ m) (hb : m<2^n)
        (hodd : Odd m) (p₀ p₁ : Component m) (hne : p₁≠p₀)
        (y₀ : Basis (transitionWidth n)) :
        outcomeMass (passed (GoodList (by omega : m≠0) hb p₀ (n^5)) y₀
          (listSuccess m n (n^5)) (target n))
          (fresh (tensorState (fairState (Nat.clog 2 m)) (n^5))
            (transitionWidth n) (2*n) (n*n^5))=(target n:ℝ) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Component, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.transitionWidth, OAI.ExactQuantumFactoring.Completion.passed, OAI.ExactQuantumFactoring.GoodList, OAI.ExactQuantumFactoring.Completion.listSuccess, OAI.ExactQuantumFactoring.Completion.target, OAI.ExactQuantumFactoring.Completion.fresh, OAI.ExactQuantumFactoring.fairState

16. theorem OAI.ExactQuantumFactoring.Completion.order_passed_mass line 134

    Source documentation

    Local same-record equalization for the literal n^5 repeated order trial.

    theorem order_passed_mass {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) (y₀ : Basis (transitionWidth n)) :
        outcomeMass (passed (fun x => orderResult s n a m (n^5) x=orderOf u) y₀
          (orderSuccess (orderOf u) (n^5)) (target n))
          (fresh (tensorState (rawState s n a m) (n^5))
            (transitionWidth n) (2*n) ((n+10)*n^5))=(target n:ℝ) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Completion.transitionWidth, OAI.ExactQuantumFactoring.Completion.passed, OAI.ExactQuantumFactoring.Completion.orderSuccess, OAI.ExactQuantumFactoring.Completion.target, OAI.ExactQuantumFactoring.Completion.fresh