Opposite errors and smaller denominators
Abstract
A unimodular pair with opposite approximation errors excludes smaller denominators.
Theorem 1.1 (The opposite error is a uniform lower bound).
Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/UnimodularApproximationBound.unimodular_opposite_error_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Let q,p and s,r be integer pairs with determinant qr-ps=1 and positive denominators. If their errors at a real slope alpha are d and -e, with d,e positive, every positive integer denominator m below q has error at least e against every integer numerator z. Integer quantities in the two error equations and conclusion are coerced to real numbers.
The determinant gives integer coordinates a,b with m=aq+bs and z=ap+br. The inequalities 0<m<q force either a positive and b negative, or a nonpositive and b positive. In both cases the absolute error ad-be is at least e.
Theorem 1.2 (Every other denominator in the gap has larger error).
Proof. Machine-checked in Lean as D5/S1/Words/Mechanical/UnimodularApproximationBound.unimodular_gap_error_bound (✓ std3). ∎
Source. Repository-derived.
Commentary.
Assume in addition that 0<s<q and e is at least twice d. For q≤m<2q+s, excluding q, 2q and q+s raises the lower bound to d+e. Integer quantities in real error equations are coerced to real numbers. The integer coordinate b is either negative, at least two, zero or one. The first two cases give the error estimate; the last two force one of the three excluded denominators.