OAI/Computability/QuantumFactoring/ContinuedFractionRecovery.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Bounded Euclidean recovery of the manuscript's nearest-bin labels. The denominator bound is logarithmic, never a search through B labels.

  1. def OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent line 16

    Source documentation

    Euclid's finite convergent recurrence, entirely natural/rational arithmetic.

    def euclidConvergent (a b : ℕ) : ℕ → ℚ
  | 0 => (a/b:ℕ)
  | k+1 => (a/b:ℕ)+(euclidConvergent b (a%b) k)⁻¹
  2. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_zero_pair line 20
  3. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_zero_left line 28
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_zero_right line 31
  5. lemma OAI.ExactQuantumFactoring.OrderTrial.real_floor_ratio line 34
  6. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_real line 40
  7. lemma OAI.ExactQuantumFactoring.OrderTrial.ratio_euclid line 51
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.euclid_two_halving line 59

    Source documentation

    Two Euclidean steps halve the denominator; the zero remainder is treated separately, since natural remainder by zero is not zero.

    lemma euclid_two_halving {b r : ℕ} (hr : 0<r) (hrb : r<b) : 2*(b%r)<b := by
…
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_terminal line 72

    Source documentation

    At most twice the denominator bit bound suffices, including rational termination and all later convergents.

    lemma euclidConvergent_terminal (s a b h : ℕ) (hb : b<2^s) :
    euclidConvergent a b (2*s+h) = (a:ℚ)/b := by
…

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent

  10. lemma OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent_bounded line 98

    Source documentation

    Every possible convergent is already in this polynomial-size list.

    lemma euclidConvergent_bounded {s a b k : ℕ} (hb : b<2^s) :
    ∃ i ≤ 2*s, euclidConvergent a b k = euclidConvergent a b i := by
…

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent

  11. lemma OAI.ExactQuantumFactoring.OrderTrial.bin_error_div line 107
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.bin_has_bounded_convergent line 119

    Source documentation

    Legendre recovery with an explicit O(log Q) search bound.

    lemma bin_has_bounded_convergent {Q d j s : ℕ}
    (hd : 0<d) (hQ : d^2<Q) (hsize : Q<2^s) (hcop : Nat.Coprime j d) :
    ∃ i ≤ 2*s, euclidConvergent (bin Q d j) Q i = (j:ℚ)/d := by
…

    Mentions: OAI.ExactQuantumFactoring.OrderTrial.euclidConvergent, OAI.ExactQuantumFactoring.OrderTrial.bin

  13. lemma OAI.ExactQuantumFactoring.OrderTrial.bin_mul_bounds line 142
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.bin_lt line 152
  15. lemma OAI.ExactQuantumFactoring.OrderTrial.same_bin_cross line 158
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.same_bin_unique line 177
  17. def OAI.ExactQuantumFactoring.OrderTrial.IsBinLabel line 190

    Source documentation

    All label checks precede evaluation of any retention expression.

    def IsBinLabel (Q B k : ℕ) (l : ℕ×ℕ) : Prop :=
…
  18. instance OAI.ExactQuantumFactoring.OrderTrial.(instance at line 193) line 193
  19. def OAI.ExactQuantumFactoring.OrderTrial.rationalLabel line 196
  20. lemma OAI.ExactQuantumFactoring.OrderTrial.rationalLabel_reduced line 198
  21. def OAI.ExactQuantumFactoring.OrderTrial.recoveredLabels line 212

    Source documentation

    Search only the polynomially many Euclidean convergents. Rational labels not satisfying the exact bin rule are rejected, not rounded into a candidate.

    def recoveredLabels (s Q B k : ℕ) : List (ℕ×ℕ) :=
…
  22. lemma OAI.ExactQuantumFactoring.OrderTrial.mem_recoveredLabels line 216
  23. lemma OAI.ExactQuantumFactoring.OrderTrial.recoveredLabels_complete line 226
  24. lemma OAI.ExactQuantumFactoring.OrderTrial.IsBinLabel.unique line 236
  25. def OAI.ExactQuantumFactoring.OrderTrial.recoverLabel line 249

    Source documentation

    The operational decoder either returns the unique exact bin label or rejects.

    def recoverLabel (s Q B k : ℕ) : Option (ℕ×ℕ) :=
…
  26. lemma OAI.ExactQuantumFactoring.OrderTrial.recoveredLabels_length line 252
  27. lemma OAI.ExactQuantumFactoring.OrderTrial.recoverLabel_sound line 256
  28. lemma OAI.ExactQuantumFactoring.OrderTrial.recoverLabel_complete line 262
  29. lemma OAI.ExactQuantumFactoring.OrderTrial.recoverLabel_iff line 273