Limits: continuity and differentiation

The limit formalism is a challenge-response protocol in which a positive tolerance in one thing must be shown to be attainable by imposing some other positive tolerance on another; a function is continuous at a specific input if, for any challenge tolerance on changes in the output, all inputs within a given response tolerance of the specific input give outputs within the challenge tolerance of the specific input's output. Likewise, a series converges if, for some given tolerance on variation between its entries, there is some point in the sequence beyond which no two entries differ by the given tolerance; and a function is differentiable at some given input, with a specified derivative, if every positive challenge tolerance on how close to the specified derivative the gradients of chords of the function must be can be met by limiting the chords to be between points within some response tolerance of the given input.

Reasoning about such challenge-response protocols typically requires use of reductio ad absurdum arguments, which I dislike; so I try to keep my use of them to a minimum. This area of my writings may be considered an implementation detail (that I dislike and wish I could replace) for things used by other areas; and shall likely grow side-discussions of how much I can get away with using more constructive methods of reasoning. In particular, for continuity and differentiation, I have a hope that one can replace the for every challenge there exists a response formulation (which leads to arguments invoking the existence of a response without necessarily showing how to construct one) with some here is a polynomial bound on the response that suffices to meet the challenge; I'm not sure how constructive the result shall be, but hope that it may at least point the way to developing some constructive mechanism that suffices.

Existing fragments:

Valid CSSValid HTML 4.01 Written by Eddy.