OAI/Computability/QuantumFactoring/QuarterPreparation.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.knownProbability_at line 19
2. def OAI.ExactQuantumFactoring.Quarter.retention line 26

   Source documentation

   The second rounding uses EXACTLY J+2, not the transition completion's slightly finer W+t+2 grid. One surplus fair retention bit is harmless.

   def retention (n : ℕ) : ℚ := quarterCoeff (n*n) (knownProbability n)

3. def OAI.ExactQuantumFactoring.Quarter.guessRetention line 27
4. abbrev OAI.ExactQuantumFactoring.Quarter.D line 28
5. abbrev OAI.ExactQuantumFactoring.Quarter.Raw line 29
6. def OAI.ExactQuantumFactoring.Quarter.fresh line 30
7. lemma OAI.ExactQuantumFactoring.Quarter.retention_at line 33
8. lemma OAI.ExactQuantumFactoring.Quarter.guessRetention_at line 37
9. def OAI.ExactQuantumFactoring.Quarter.ordinaryPass line 49
10. def OAI.ExactQuantumFactoring.Quarter.guessPass line 51
11. def OAI.ExactQuantumFactoring.Quarter.passed line 54
12. theorem OAI.ExactQuantumFactoring.Quarter.passed_mass line 57
13. theorem OAI.ExactQuantumFactoring.Quarter.passed_correct line 110

    Source documentation

    The flagged output always has the same canonical root encoding.

    theorem passed_correct {α : Type*} {N n : ℕ} (ordinary : α→Basis (n*n)) (success : α→Prop)
        (hsound : ∀ a,success a → CorrectEncoding N n (guessWords n (ordinary a)))
        (r : Raw α n) (h : passed N success r) :
        CorrectEncoding N n (guessWords n (Completion.output ordinary r)) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.guessWords, OAI.ExactQuantumFactoring.Quarter.Raw, OAI.ExactQuantumFactoring.Quarter.passed, OAI.ExactQuantumFactoring.Completion.output

14. def OAI.ExactQuantumFactoring.Quarter.program line 119

    Source documentation

    No probability or canonical factor list occurs in the raw unitary.

    def program {q : ℕ} (P : List (Instruction q)) (n : ℕ) := Completion.program P (n*n) 1 (n^11)

    Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.Completion.program

15. lemma OAI.ExactQuantumFactoring.Quarter.program_entry line 120
16. lemma OAI.ExactQuantumFactoring.Quarter.program_length line 125