rite(ef): give Pentecost, its Vigil and Christ the King their week

named hardcoded week = None for ef-pentecost-vigil, ef-pentecost and
ef-christ-the-king, unlike the five sibling named Sundays (Easter, Low
Sunday, Passion Sunday, Palm Sunday, Trinity), which already carry the
explicit week number that week computes for the same date. Because these
three sit inside a season run rather than at a run boundary, the omission let
the week number jump on the following Monday without an intervening Sunday
marking the change -- breaking week continuity in every single year in the
domain.

This was found by the new Validate invariant harness (Task 14), which
flagged exactly two failures in every one of the 8416 years 1583..9998, both
on the Monday after one of these days. Season contiguity itself was clean
across the whole domain; only week numbering was affected.

Pentecost and its Vigil are fixed Easter offsets, so they take the literal
values (7 and 8) that week already computes for them. Christ the King's date
varies by year, so the same expression week evaluates is inlined instead,
since week is defined later in the file and cannot be called from named.

Added a general property test, prop_named_week_agrees_with_week, checking
across 200 random years that wherever named gives an explicit week, it
matches what week independently computes for that date -- covering all
sibling entries, not just the three fixed here, so the same drift cannot
silently reappear in a future addition to named.

1 files changed, 19 insertions, 3 deletions

diff --git a/lib/rites/rite_ef/temporal_ef.ml b/lib/rites/rite_ef/temporal_ef.ml
index 4eac99f..4147278 100644
--- a/lib/rites/rite_ef/temporal_ef.ml
+++ b/lib/rites/rite_ef/temporal_ef.ml
@@ -95,15 +95,31 @@ let named d =
     Some (Paschaltide, "ef-ascension-vigil", Colour.White, Class2, None)
   else if same d (off 39) then Some (Paschaltide, "ef-ascension", Colour.White, Class1, None)
   else if same d (off 48) then
-    Some (Paschaltide, "ef-pentecost-vigil", Colour.Red, Class1, None) (* RG 91 entry 9 *)
-  else if same d (off 49) then Some (Paschaltide, "ef-pentecost", Colour.Red, Class1, None)
+    (* Carries week 7 -- the same week as the Friday before it -- for
+       consistency with the other named Sundays here (Easter, Low Sunday,
+       Trinity below): a named day inside a season run must not interrupt the
+       run's week continuity. Not an RG rule, an internal-consistency one;
+       this was [None] until the Validate invariant harness (Task 14) caught
+       the resulting jump on the following Monday. *)
+    Some (Paschaltide, "ef-pentecost-vigil", Colour.Red, Class1, Some 7) (* RG 91 entry 9 *)
+  else if same d (off 49) then
+    (* Carries week 8, for the same reason as the Vigil just above. *)
+    Some (Paschaltide, "ef-pentecost", Colour.Red, Class1, Some 8)
   else if same d (off 56) then Some (Time_after_pentecost, "ef-trinity", Colour.White, Class1, Some 1)
   else if same d (off 60) then
     Some (Time_after_pentecost, "ef-corpus-christi", Colour.White, Class1, None)
   else if same d (off 68) then
     Some (Time_after_pentecost, "ef-sacred-heart", Colour.White, Class1, None)
   else if same d (christ_the_king y) then
-    Some (Time_after_pentecost, "ef-christ-the-king", Colour.White, Class1, None)
+    (* Carries its computed week number too, for the same internal-consistency
+       reason as Pentecost above -- caught by the same Validate finding.
+       Unlike Pentecost this isn't a fixed Easter-offset, so it can't be a
+       literal; [week] below computes it but is defined later in this file and
+       can't be called from here, so the same expression is inlined here.
+       test_named_week_agrees_with_week pins the two together. *)
+    let pentecost = off 49 in
+    Some (Time_after_pentecost, "ef-christ-the-king", Colour.White, Class1,
+          Some ((Date.to_rata d - Date.to_rata pentecost) / 7))
   else None
 
 let days_between a b = Date.to_rata b - Date.to_rata a