OAI/Computability/QuantumFactoring/Exactness.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.minusI line 12

   Source documentation

   Integer arithmetic at grid points. The only root of unity is -i.

   def minusI : GaussianInt := ⟨0,-1⟩

2. lemma OAI.ExactQuantumFactoring.OrderTrial.minusI_cast line 14
3. def OAI.ExactQuantumFactoring.OrderTrial.gridPhaseNumerator line 17
4. lemma OAI.ExactQuantumFactoring.OrderTrial.phase_grid_numerator line 21
5. def OAI.ExactQuantumFactoring.OrderTrial.residueGaussianNumerator line 46

   Source documentation

   A literal finite integer sum, used to prove dyadicity independently of the bounded-piece evaluator. This sum is NOT asserted to be polynomial-time.

   def residueGaussianNumerator (Q d j t : ℕ) : GaussianInt :=
   …

6. def OAI.ExactQuantumFactoring.OrderTrial.residueProbabilityRat line 49
7. lemma OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude_gaussian line 52
8. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbabilityRat_cast line 64
9. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbabilityRat_nonneg line 72
10. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbabilityRat_le_one line 76
11. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbability_dyadic line 84
12. lemma OAI.ExactQuantumFactoring.OrderTrial.residueProbability_numerator_bounds line 90

    Source documentation

    An explicit 4b-bit denominator, and numerator bounded by that denominator.

    lemma residueProbability_numerator_bounds {Q : ℕ} (hQ : 0 < Q) (d j t : ℕ) :
        0 ≤ (residueGaussianNumerator Q d j t).norm ∧
          (residueGaussianNumerator Q d j t).norm ≤ (Q:ℤ)^4 := by
    …

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.residueGaussianNumerator

13. def OAI.ExactQuantumFactoring.OrderTrial.phaseLabel line 104
14. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseLabel_mod line 106
15. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseLabel_tile line 110
16. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseLabel_correlation line 115
17. lemma OAI.ExactQuantumFactoring.OrderTrial.sum_range_tiles line 144
18. lemma OAI.ExactQuantumFactoring.OrderTrial.sum_if_carry line 152
19. def OAI.ExactQuantumFactoring.OrderTrial.phaseOverlapSum line 174

    Source documentation

    Unnormalized correlation of the exactly prepared quarter-step state.

    noncomputable def phaseOverlapSum (m D : ℕ) : ℂ :=
    …

20. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseOverlapSum_eq line 177
21. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseOverlap_eq line 203

    Source documentation

    Exact overlap, with its direction fixed by the forward shift.

    lemma phaseOverlap_eq {m : ℕ} (hm : 0 < m) (D : ℕ) :
        phaseOverlapSum m D/(4*(m:ℂ)) = phase ((D:ℝ)/(4*(m:ℝ))) := by
    …

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.phaseOverlapSum, OAI.ExactQuantumFactoring.OrderTrial.phase

22. def OAI.ExactQuantumFactoring.OrderTrial.phaseState line 226
23. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseState_overlap line 229
24. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseState_normalized line 245
25. def OAI.ExactQuantumFactoring.Exactness.completionCoeff line 266

    Source documentation

    Source (completion), with its actual downward integer rounding.

    def completionCoeff (E : ℕ) (z A : ℚ) : ℚ :=
    …

26. def OAI.ExactQuantumFactoring.Exactness.completionRemainder line 269
27. lemma OAI.ExactQuantumFactoring.Exactness.completion_rounding line 271
28. lemma OAI.ExactQuantumFactoring.Exactness.completion_mass line 303

    Source documentation

    Both branch masses include the choice of branch and the guessing probability.

    lemma completion_mass (W t : ℕ) (s z : ℚ) :
        (1-1/(2:ℚ)^t)*s * completionCoeff (W+t+2) z ((1-1/(2:ℚ)^t)*s) +
        (1/(2:ℚ)^t)*(1/(2:ℚ)^W)*
          (completionRemainder (W+t+2) z ((1-1/(2:ℚ)^t)*s)*(2:ℚ)^W/(1/(2:ℚ)^t)) = z := by
    …

    Mentions: OAI.ExactQuantumFactoring.Exactness.completionCoeff, OAI.ExactQuantumFactoring.Exactness.completionRemainder

29. lemma OAI.ExactQuantumFactoring.Exactness.completion_retention_bounds line 311
30. def OAI.ExactQuantumFactoring.Exactness.quarterCoeff line 340

    Source documentation

    The second rounding of Section 6, independent of the transition algorithm.

    def quarterCoeff (J : ℕ) (p : ℚ) : ℚ := completionCoeff (J+2) (1/2) p

    Mentions: OAI.ExactQuantumFactoring.Exactness.completionCoeff

31. def OAI.ExactQuantumFactoring.Exactness.quarterRemainder line 342
32. lemma OAI.ExactQuantumFactoring.Exactness.quarter_retention_bounds line 344
33. lemma OAI.ExactQuantumFactoring.Exactness.quarter_mass line 364
34. lemma OAI.ExactQuantumFactoring.Exactness.step_tenth_power_bound line 373

    Source documentation

    An explicit elementary discrete bound eliminates a real-calculus asymptotic.

    lemma step_tenth_power_bound {n : ℕ} (hn : 128 ≤ n) : (n+1)^10 ≤ 2*n^10 := by
    …

35. lemma OAI.ExactQuantumFactoring.Exactness.tenth_power_exponential line 385
36. def OAI.ExactQuantumFactoring.Exactness.knownProbability line 395
37. lemma OAI.ExactQuantumFactoring.Exactness.knownProbability_bounds line 397