Follow-ups from merged slices: leap table refresh, proved vectors, and cross-check standing #6

Follow-ups from the merged RFC slices.

PR #2: The Go and RFC cross-check is marked as a one-off comparison, not part of the bar. Record whether that standing is intended, or whether the cross-check joins the bar later.

PR #3: The year-start grid covers 0096-12-31 in the differential run only. It is not a proved vector. Is a proved vector planned for that day, or is differential coverage the intended level?

PR #4: The leap second table expires on 2027-06-28. No step for refreshing the table after that date is recorded. The code keeps its own list of 27 year and month pairs and never reads the spec table. Record where a reader finds the theorem that proves the two agree, or add a named theorem for it.

PR #5: After the nanoda workaround, record whether any kernel still exercises the parser on the long examples, or whether those vectors rest on the parseExt equivalence statement alone. Is a worked example planned for an application with a different tag set from the example Processor in the spec, or is none planned?

Automated posting by agentic team with human oversight.

Current work

The draft records refresh procedures and adds a proved calendar vector.

Awaiting independent review: #9.