Reciprocal Refinement
Theorem:
(defthm recip-refinement-1 (let* ((e1 (rne (- 1 (* b y1)) p)) (y3p (+ y1 (* e1 y2))) (ep3p (* ep1 (+ ep2 (* (expt 2 (- p)) (1+ ep2)))))) (implies (and (rationalp y1) (rationalp y2) (rationalp b) (rationalp ep1) (rationalp ep2) (integerp p) (> p 0) (<= (abs (- 1 (* b y1))) ep1) (<= (abs (- 1 (* b y2))) ep2)) (<= (abs (- 1 (* b y3p))) ep3p))) :rule-classes nil)
Theorem:
(defthm recip-refinement-2 (let* ((e1 (rne (- 1 (* b y1)) p)) (y3p (+ y1 (* e1 y2))) (y3 (rne y3p p)) (ep3p (* ep1 (+ ep2 (* (expt 2 (- p)) (1+ ep2))))) (ep3 (+ ep3p (* (expt 2 (- p)) (1+ ep3p))))) (implies (and (rationalp y1) (rationalp y2) (rationalp b) (rationalp ep1) (rationalp ep2) (integerp p) (> p 0) (<= (abs (- 1 (* b y1))) ep1) (<= (abs (- 1 (* b y2))) ep2)) (<= (abs (- 1 (* b y3))) ep3))) :rule-classes nil)
Function:
(defun h-excps (d p) (if (zp d) nil (cons (- 2 (* (expt 2 (- 1 p)) d)) (h-excps (1- d) p))))
Theorem:
(defthm harrison-lemma (let ((y (rne yp p)) (d (cg (* (expt 2 (* 2 p)) ep)))) (implies (and (rationalp b) (rationalp yp) (rationalp ep) (integerp p) (> p 1) (<= 1 b) (< b 2) (exactp b p) (not (member b (h-excps d p))) (< ep (expt 2 (- (1+ p)))) (<= (abs (- 1 (* b yp))) ep)) (< (abs (- 1 (* b y))) (expt 2 (- p))))) :rule-classes nil)