[LEAPSECS] BBC radio Crowd Science

[Warner Losh]

On Sat, Feb 4, 2017 at 8:37 AM, Clive D.W. Feather <clive at davros.org> wrote:
> Now define the "linearization" of a broken-down time as:
>
>     L = D*86400 + H*3600 + M*60 + S
>
> In TAI, L is the number of seconds since 00:00:00 on the epoch date.
>
> In UTC L is *NOT* the number of seconds since anything useful, but is rather
> just a number that turns out to be useful. With an epoch date of 1970-01-01,
> L gives you the Posix time_t value, but that is not relevant here. It *is*
> important to note that the calculation of L in UTC is lossy in two different
> ways:
> * at a positive leap second, the same L value represents two different times;
> * at a negative leap seconds, some L values don't represent any possible
>   time.
> As we will see, this lossiness turns out not to matter.

That's where you lose me. I believe that it actually does matter since
you encode the extra offset for the leap second into the
linearization, you've hidden the delta such that you have to define
the offset as changing after the leap second for it to work out. I
contend that since the mapping / linearization isn't 1:1 onto, the
proof is not valid. I think this is the crux of my problem with Tom's
answer to my first leap second question. We have two times, that are
obviously different that when subtracted produce 0 as the answer. x-y
= 0 should only be true when x and y are the same. But we get that
answer when they are different. I believe this is can only happen with
a partial ordering. Since UTC is not a partial ordering of the
seconds, I'm not sure that I buy this argument as definitive.

I'll concede this is a convenient computationally.

Warner