[tz] What's "right"?

[Michael H Deckers]

    On 2020-11-16 14:15, John Sauter wrote:

> In addition, following Steve Allen's suggestion, the start of the leap
> second in the time scale after the step could be 2017-01-00T23:59:59.


    Yes, it is.

    But I am not aware of an official definition of what a leap
    second is.

    A positive leap second is usually taken to be a (left closed
    and right open) interval of length 1 s of TAI values that
    are not associated with UTC values by the function from UTC
    to TAI as published by the IERS. For the latest leap second this
    interval was [2017-01-01T00:00:36..2017-01-01T00:00:37[;
    while TAI was in that interval, UTC could be 36 s or 37 s
    less than TAI, and ITU recommends the use of their leap second
    notation for the value of UTC.

    Michael Deckers.