BTW Your second statement of theorem 1 is again wrong
Since f(x)=x is continuous the John's counterexample is
again working.
f(x) is a function defined by an expression in the John's
wording.
F(X) is THE extension calculated by a interval
transcription of the expression.
Then for F(X) the isotonicity holds.
(a) I was about to point out the same two things. It's what I'm calling
the "natural interval extension" (Arnold asserts this is standard
terminology), aka what you call "straightforward interval computation"
that is isotonic.
And even that is only conditionally true.
IF the interval version of each elementary function is isotonic
THEN any function constructed from them by "straightforward interval
computation" is isotonic.
But if we define the interval version of EVERY elementary function
stupidly as in my counterexample (e.g. Entire if 0 not in xx, something
sensible otherwise) then obviously this applies to functions defined by
"straightforward interval computation" too, so isotonicity fails
spectacularly.
I seem to recall discussion by elementary-function experts that
isotonicity can fail "at the margins", i.e. by an ULP (unit in last
place) or two, if a point elementary function e(x), used in coding its
interval version, is "wobbly". E.g. if it is<1 ULP away from correct
value at one FP number, and>2 ULPs away at the next FP number. So there's
a nontrivial risk of isotonicity failing thanks to defects in library
functions.
(b) You say "the decoration systems of motions 25-26 are too
sophisticated...". I rather agree. However I think your, and Dominique's,
desire to remove the "containment order" is more about presentation than
substance.
Like death and taxes, the "containment" order is a fact of life. It
simply expresses the fact that, because of interval widening due to
dependence, the computed decoration fact may not be the sharpest one that
actually holds. E.g. in your current scheme
saf may be true but you actually compute def (which is valid but
weaker).
saf may be true but you actually compute enc ...
def may be true but you actually compute enc ...
ndf may be true but you actually compute enc ...
Would you prefer it if the standard says something like the following?
The computed decoration always makes a true statement about the
continuity, definedness, etc., of the function f over the box xx.
However it may not be the strongest one available [give example] ... By
introducing a *containment order* and the notion of the *exact
decoration of f over xx *, one may express this in the form of a
*FTDIA*, which says that the computed interval yy and decoration d,
resulting from evaluating f(xx), _jointly_ enclose the exact range and
exact decoration, respectively, of f over xx. [followed by fuller
explanation]...
(* meaning bold introducing a new concept, _ meaning italic for
emphasis.)
This presents the FTDIA as an optional interpretation that one may find
enlightening, and the containment order as symbolically expressing an
unfortunate fact of life in the same way as
(take-home pay T)< (gross pay G)
symbolically expresses another unfortunate fact.
John