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
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.