Prove early calendar vector and record verification boundaries

Proofs/FromUnix/Main.lean

@@ -119,6 +119,7 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) :
     omega
 
 theorem Spec.fromUnixSeconds_vectors :
+    Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧

README.md

@@ -50,7 +50,7 @@ The statements are in `Spec.lean`. The definitions they use, written from the RF
 | A leap second comes after second 59 and before the next minute, fraction included. Its Unix seconds equal those of the second after it. | `Spec.leap_second_order` |
 | `fromUnixSeconds` turns whole seconds since the epoch back into a timestamp: the one, at most one, that is valid, in UTC, with no fraction and no leap second, and names those seconds. Its date arithmetic is checked against the same day count. | `Spec.fromUnixSeconds_iff` |
 | `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z, and `none` outside them. | `Spec.fromUnixSeconds_isSome` |
-| `fromUnixSeconds` gives the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` |
+| `fromUnixSeconds` gives 0096-12-31T00:00:00Z, the epoch, the section 5.8 example, 2000-02-29, 2038-01-19T03:14:07Z for the last second of a signed 32-bit count, the second before the epoch, and both ends of the range, and gives `none` one second past each end. | `Spec.fromUnixSeconds_vectors` |
 | The calendar, leap second, and syntax cases: 29 February in 1900, 2000 and 2001; second 60 at and away from a month's end; lower case `t` and `z`; a space for `T`; a comma; an offset of `+24:00`; trailing text. | `Spec.calendar_vectors`, `Spec.leap_second_vectors`, `Spec.syntax_vectors` |
 | `isValidKnown` decides section 5.7 with the table of leap seconds. It allows second 60 only at one of the table's leap seconds, at the same instant whatever the offset. The table is the one in `Spec/Leap.lean`. The code keeps its own list of months, and the proof shows the two agree. | `Spec.isValidKnown_iff` |
 | `siSeconds` is the Unix seconds since 1972-01-01T00:00:00Z, and one more for each leap second of the table before the timestamp. From 1972 on, those are the SI seconds; so a leap second, the second before it and the second after it get three numbers in a row. Before 1972 the number is Unix seconds, 86400 to a day. | `Spec.siSeconds_eq` |

SPEC.md

@@ -125,7 +125,7 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions
 | Lower case `t` and `z` are read; a space for `T`, a missing part, a comma, an out-of-range offset and trailing text are not. | `Spec.syntax_vectors` |
 | `fromUnixSeconds s` is `t` exactly when `t` is valid, in UTC, with no fraction and a second of at most 59, and names `s`. | `Spec.fromUnixSeconds_iff` |
 | `fromUnixSeconds` gives a timestamp exactly for the seconds from 0000-01-01T00:00:00Z to 9999-12-31T23:59:59Z. | `Spec.fromUnixSeconds_isSome` |
-| The epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` |
+| 0096-12-31 at midnight, the epoch, the section 5.8 example, a leap day, the last second of a signed 32-bit count, the second before the epoch, and the ends of the range and one second past each. | `Spec.fromUnixSeconds_vectors` |
 | `isValidKnown` decides `Spec.ValidKnown`: `Spec.Valid`, with second 60 only at a leap second of the table. | `Spec.isValidKnown_iff` |
 | `siSeconds` is Unix seconds since 1972 and one more for each leap second of the table before the timestamp. | `Spec.siSeconds_eq` |
 | On whole seconds valid by the table, `siSeconds` gives the order of the instants. | `Spec.siSeconds_order` |
@@ -159,3 +159,29 @@ The differential tests compare the tool with these oracles:
 - A copy of the rules above, written in Python from the RFC.
 - For leap seconds, tzdata's `leap-seconds.list` on the test machine, read by the test script itself, with the SI seconds and TAI − UTC worked out from it in Python.
 - For RFC 9557, the grammar of section 4.1 and the rules of sections 3.2 to 3.4, written in Python from the RFC, with the same example application.
+
+## Follow-up verification record
+
+`Rfc3339.Proofs.Leap.leapKey_table` in `Proofs/Leap/Table.lean`
+proves that the implementation's ordered list of leap-second keys equals
+the keys derived from `Spec.leapTable.tail`. `Spec.isValidKnown_iff` uses
+that equality. The literal table's agreement with IERS remains trusted.
+
+Before the table expires on 28 June 2027, obtain the current IERS Bulletin C
+and tzdata leap-seconds.list, compare the literal table in `Spec/Leap.lean`,
+and update its source and expiry record. If an entry changes, update
+`Rfc3339/Leap.lean` in the same change, rebuild the table equality proof,
+and rerun the full bar and differential suite. Have a spec reviewer check
+the replacement source. Expiry alone does not announce a leap second.
+
+The external Go, Temporal and ERFA cross-check remains a one-off comparison
+(`tests/CROSS-CHECK.md`), outside the verified bar. The 0096-12-31 UTC
+midnight case is now also a kernel-computed `Spec.fromUnixSeconds_vectors`
+case, rather than only a differential calendar-grid case.
+
+The long IXDTF vectors in `Proofs/Ixdtf/Main.lean` use `vx_validB_sound`
+and the parser equivalence proof; they do not directly execute the whole
+parser in the kernel. Their shorter timestamp components and grammar
+checks are kernel-computed. The existing processor vectors are examples
+of one tag policy; this slice provides no worked alternative tag-set
+application. `Spec.erroneous_iff` quantifies over every `Processor`.

Spec.lean

@@ -162,10 +162,12 @@ theorem Spec.fromUnixSeconds_isSome (s : Int) :
       Spec.unixSeconds ⟨0, 1, 1, 0, 0, 0, [], .z⟩ ≤ s ∧
         s ≤ Spec.unixSeconds ⟨9999, 12, 31, 23, 59, 59, [], .z⟩ := sorry
 
-/-- The epoch; the example of section 5.8; a leap day; the last second a
+/-- 0096-12-31 at midnight, from the year-start grid; the epoch; the
+    example of section 5.8; a leap day; the last second a
     signed 32-bit count reaches; the second before the epoch; the ends of
     the range, and one second past each. -/
 theorem Spec.fromUnixSeconds_vectors :
+    Rfc3339.fromUnixSeconds (-59106153600) = some ⟨96, 12, 31, 0, 0, 0, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 0 = some ⟨1970, 1, 1, 0, 0, 0, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 482196050 = some ⟨1985, 4, 12, 23, 20, 50, [], .z⟩ ∧
     Rfc3339.fromUnixSeconds 951782400 = some ⟨2000, 2, 29, 0, 0, 0, [], .z⟩ ∧