rite(ef): fix duplicate slugs and omitted weeks in the temporal cycle

Two correctness bugs in Temporal_ef, both only visible across many
years, not a single point assertion:

1. Duplicate slugs within one liturgical year. Christmastide has no
   numbered weeks, so the ferial fallback's <season>-<week>-<weekday>
   scheme collapsed every feria in it to literal week "0". Since
   colitur's Christmastide runs 25 Dec - 13 Jan (RG 72-73, a deliberate
   divergence from lectio), the same weekday recurs across that span
   and the keys collided (e.g. ef-christmas-0-saturday on three
   different dates). Fixed with a dedicated christmastide_feria_slug
   that splits the span into four sub-stretches, prioritising
   compatibility with lectio's own keys wherever lectio has one:
     - 26-28 Dec keeps lectio's existing ef-christmas-0-<weekday>.
     - 2-5 Jan becomes ef-christmas-1-<weekday> -- lectio collapses
       this indistinguishably into the same key as the stretch above,
       so there is nothing to preserve; a colitur-only lectionary gap.
     - 7-13 Jan splits at the actual first-Sunday-after-Epiphany
       origin: on/after it, this is genuinely week 1 of Time after
       Epiphany and takes lectio's own ef-time-after-epiphany-1-<weekday>
       (which also can't collide with that season's own later week-1
       ferias, since it's the same computation). Before it (0-6 days,
       whenever Epiphany doesn't fall on a Saturday), a first attempt
       at labelling this "week 1" too, matching a literal reading of
       lectio's behaviour, was verified empirically (a throwaway sweep
       of the full 1583..9998 domain) to reproduce duplicates in most
       years -- so this remainder is its own ef-christmas-2-<weekday>,
       a further colitur-only gap.
   Verified with the same throwaway sweep: zero duplicate slugs across
   1583..9998 after the fix.

2. named's week field was set by hand on some branches (Passion/Palm
   Sunday, Easter, Low Sunday, Pentecost and its Vigil, Christ the
   King) and left at None on others (Ascension and its Vigil, Corpus
   Christi, Sacred Heart) even though all of them sit inside a
   numbered season run. named no longer carries a week at all --
   temporal now calls week itself for every day, named or not, so "a
   named day inside a run carries that run's week" holds by
   construction rather than by remembering to set it on each branch.
   temporal.mli's week field doc is reworded to state the actual rule.

Covering tests: point assertions for all four Christmastide
sub-stretches; a QCheck property scanning random years for any
duplicate slug within a liturgical year (excluding the deliberate
resumed-Sunday reuse); point assertions for the four previously-None
days now carrying their week (first to fail without the fix: Ascension
Vigil, expected Some 6, got None); a QCheck property asserting
temporal's week equals week for every day of the year, replacing a
prior property whose fallback made it structurally incapable of
detecting an omitted week.

Also: cite RG 91 e18 for the September/Advent Ember days matching
lectio and flag the Lent/Whitsun Ember and Rogation slugs as
colitur-only lectionary gaps inline, matching the existing
Nativity-vigil/octave-day convention; cite RG 117/123/127/128/131 for
season colours and Gaudete/Laetare rose; drop the unreachable
Passiontide arm from the Sunday-rank match (Passiontide has only two
Sundays and both are already named above, so no Passiontide Sunday
ever reaches that fallback).

1 files changed, 187 insertions, 74 deletions

diff --git a/lib/rites/rite_ef/temporal_ef.ml b/lib/rites/rite_ef/temporal_ef.ml
index 4147278..52a9adb 100644
--- a/lib/rites/rite_ef/temporal_ef.ml
+++ b/lib/rites/rite_ef/temporal_ef.ml
@@ -59,67 +59,56 @@ let same a b = Date.compare a b = 0
    Sunday (RG 91 entry 6), Ash Wednesday (RG 91 entry 7), and the days within
    the Octave of the Nativity (RG 63-70, RG 91 entry 17).
 
-   Returns (season, slug, colour, rank, week). *)
+   Returns (season, slug, colour, rank). Deliberately NOT week: an earlier
+   version carried an explicit week option here, hand-set on some branches
+   (Passion/Palm Sunday, Easter, Low Sunday, Pentecost and its Vigil, Christ
+   the King) and left at [None] on others (Ascension and its Vigil, Corpus
+   Christi, Sacred Heart) even though those sit inside a numbered season run
+   just the same -- a manual-convention bug the guarding property could not
+   even detect (see test_temporal_ef.ml's history). [temporal] now calls
+   [week] itself for every day, named or not, which makes "a named day inside
+   a run carries that run's week" hold by construction instead of by
+   remembering to set it here. *)
 let named d =
   let y = Date.year d in
   let easter = Computus.gregorian_easter y in
   let off n = Date.add_days easter n in
   let m = Date.month d and dd = Date.day d in
-  if m = 12 && dd = 25 then Some (Christmastide, "ef-nativity", Colour.White, Class1, None)
+  if m = 12 && dd = 25 then Some (Christmastide, "ef-nativity", Colour.White, Class1)
   else if m = 12 && dd = 24 then
     (* RG 91 entry 5: the Vigil of the Nativity is I class. lectio has no slug
        for it, so this key has no lectionary entry until Plan 3 fills it. *)
-    Some (Advent, "ef-nativity-vigil", Colour.Violet, Class1, None)
+    Some (Advent, "ef-nativity-vigil", Colour.Violet, Class1)
   else if m = 12 && (dd = 29 || dd = 30 || dd = 31) then
     (* Days within the Octave of the Nativity; 26-28 Dec are Stephen, John and
        the Innocents, hence sanctoral (Plan 3). Colitur slugs -- lectionary gap. *)
-    Some (Christmastide, Printf.sprintf "ef-nativity-octave-day-%d" (dd - 24), Colour.White, Class2, None)
+    Some (Christmastide, Printf.sprintf "ef-nativity-octave-day-%d" (dd - 24), Colour.White, Class2)
   else if m = 1 && dd = 1 then
     (* RG 91 entry 5: 1 Jan is the Octave Day of the Nativity, the same table
        entry as the Nativity vigil above. *)
-    Some (Christmastide, "ef-circumcision", Colour.White, Class1, None)
-  else if m = 1 && dd = 6 then Some (Christmastide, "ef-epiphany", Colour.White, Class1, None)
+    Some (Christmastide, "ef-circumcision", Colour.White, Class1)
+  else if m = 1 && dd = 6 then Some (Christmastide, "ef-epiphany", Colour.White, Class1)
   else if same d (off (-46)) then
-    Some (Lent, "ef-ash-wednesday", Colour.Violet, Class1, None) (* RG 91 entry 7 *)
+    Some (Lent, "ef-ash-wednesday", Colour.Violet, Class1) (* RG 91 entry 7 *)
   else if same d (off (-14)) then
-    Some (Passiontide, "ef-passion-sunday", Colour.Violet, Class1, Some 1) (* RG 91 entry 6 *)
+    Some (Passiontide, "ef-passion-sunday", Colour.Violet, Class1) (* RG 91 entry 6 *)
   else if same d (off (-7)) then
-    Some (Passiontide, "ef-palm-sunday", Colour.Violet, Class1, Some 2) (* RG 91 entry 6 *)
-  else if same d easter then Some (Paschaltide, "ef-easter-sunday", Colour.White, Class1, Some 1)
+    Some (Passiontide, "ef-palm-sunday", Colour.Violet, Class1) (* RG 91 entry 6 *)
+  else if same d easter then Some (Paschaltide, "ef-easter-sunday", Colour.White, Class1)
   else if same d (off 7) then
-    Some (Paschaltide, "ef-low-sunday", Colour.White, Class1, Some 2) (* RG 91 entry 6 *)
+    Some (Paschaltide, "ef-low-sunday", Colour.White, Class1) (* RG 91 entry 6 *)
   else if same d (off 38) then
     (* RG 91 entry 21: II-class vigil. It is also Rogation Wednesday; with no
        precedence framework until Plan 3, temporal emits the higher-ranked
        vigil and the Rogation commemoration waits for RG 108-111. *)
-    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
-    (* 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
-    (* 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))
+    Some (Paschaltide, "ef-ascension-vigil", Colour.White, Class2)
+  else if same d (off 39) then Some (Paschaltide, "ef-ascension", Colour.White, Class1)
+  else if same d (off 48) then Some (Paschaltide, "ef-pentecost-vigil", Colour.Red, Class1) (* RG 91 entry 9 *)
+  else if same d (off 49) then Some (Paschaltide, "ef-pentecost", Colour.Red, Class1)
+  else if same d (off 56) then Some (Time_after_pentecost, "ef-trinity", Colour.White, Class1)
+  else if same d (off 60) then Some (Time_after_pentecost, "ef-corpus-christi", Colour.White, Class1)
+  else if same d (off 68) then Some (Time_after_pentecost, "ef-sacred-heart", Colour.White, Class1)
+  else if same d (christ_the_king y) then Some (Time_after_pentecost, "ef-christ-the-king", Colour.White, Class1)
   else None
 
 let days_between a b = Date.to_rata b - Date.to_rata a
@@ -150,6 +139,12 @@ let week_origin s y =
   | Paschaltide -> Some easter
   | Time_after_pentecost -> Some (Date.add_days easter 49) (* Pentecost *)
 
+(* [week] is total and defined for every date, named or not: a named day
+   inside a numbered season run carries that run's week by calling this same
+   function, not by a separately hand-set value (see [named]'s docstring
+   above). It naturally returns [None] for Christmastide (no season-wide
+   numbering) and for the handful of proper-Mass days between Ash Wednesday
+   and Lent I that precede any run's origin. *)
 let week d =
   let s = season d in
   match week_origin s (Date.year d) with
@@ -159,6 +154,56 @@ let week d =
       let n = match s with Time_after_pentecost -> n | _ -> n + 1 in
       if n < 1 then None else Some n
 
+(* Christmastide has no numbered weeks ([week_origin] returns [None]), so the
+   generic <season>-<week>-<weekday> ferial fallback below would collapse
+   every feria to literal week "0" -- and because colitur's Christmastide
+   spans 25 Dec - 13 Jan (RG 72-73, the deliberate divergence from lectio),
+   the same weekday recurs two or three times across that span, producing
+   duplicate slugs within a single liturgical year (register finding 1).
+   Four sub-stretches, each given a key that cannot collide with the others:
+
+   - 26-28 Dec (between the Nativity and its Octave days, which are named
+     above): lectio has no narrower key here either, so this keeps its
+     existing "ef-christmas-0-<weekday>" key unchanged -- nothing to lose by
+     changing it, and nothing gained.
+   - 2-5 Jan (between the Octave Day and Epiphany): lectio *also* collapses
+     this to "ef-christmas-0-<weekday>", indistinguishable from the stretch
+     above in lectio's own data. colitur cannot preserve a distinction lectio
+     doesn't make, so this becomes "ef-christmas-1-<weekday>" -- a
+     colitur-only key and a lectionary gap for the Plan 3 bootstrap to fill,
+     exactly like the Nativity vigil and octave-day keys above.
+   - 7-13 Jan, split in two by the *actual* first-Sunday-after-Epiphany
+     origin ([week_origin Time_after_epiphany], which by construction always
+     falls somewhere in this window -- see that function's own comment):
+       - from the origin Sunday through 13 Jan: this genuinely is week 1 of
+         Time after Epiphany, just still inside Christmastide by season
+         (RG 72-73). lectio keys it "ef-time-after-epiphany-1-<weekday>", the
+         same key [sunday_slug] already gives the Sunday in this window --
+         and it is the *same computation* the ordinary Time-after-Epiphany
+         ferial fallback below will give the rest of that same
+         Sunday-to-Saturday week once the season turns on 14 Jan, so this
+         cannot collide with it (a fixed 7-day week has each weekday once).
+       - 7 Jan through the day *before* the origin (0-6 days, only present
+         when Epiphany does not fall on a Saturday): these genuinely precede
+         week 1 -- treating them as week 1 too, as a naive calendar-range
+         read of lectio's behaviour would, collides with the days named just
+         above, because they are exactly 7 days before them for whichever
+         weekdays they cover (verified empirically: reusing "week 1" here
+         produced duplicates in most years, not merely an edge case). No
+         lectio key to preserve either way, so this is its own colitur-only
+         "ef-christmas-2-<weekday>" -- a further lectionary gap. *)
+let christmastide_feria_slug d =
+  let y = Date.year d in
+  let m = Date.month d and dd = Date.day d in
+  let w = Date.weekday_to_string (Date.weekday d) in
+  if m = 12 && dd >= 26 && dd <= 28 then Some (Printf.sprintf "ef-christmas-0-%s" w)
+  else if m = 1 && dd >= 2 && dd <= 5 then Some (Printf.sprintf "ef-christmas-1-%s" w)
+  else if m = 1 && dd >= 7 && dd <= 13 then
+    match week_origin Time_after_epiphany y with
+    | Some origin when Date.compare d origin >= 0 -> Some (Printf.sprintf "ef-time-after-epiphany-1-%s" w)
+    | _ -> Some (Printf.sprintf "ef-christmas-2-%s" w)
+  else None
+
 (* Sunday slugs. These are lectionary keys: they use [season_slug_word], and for
    Christmastide they keep lectio's keys even though colitur's season differs
    (spec §4.4 -- slugs are opaque keys, not truth). *)
@@ -206,7 +251,20 @@ let sunday_slug d =
 
 let id = "ef"
 
-(* The third Sunday of September: the Ember week's anchor. *)
+(* The third Sunday of September: the Ember week's anchor.
+
+   This specific date-derivation rule is one of the more contested points in
+   the 1962 calendar: pre-1955 practice tied the September Ember days to the
+   week following the Exaltation of the Holy Cross (14 Sept) instead. The two
+   rules only disagree when 1 September is a Monday -- 2025 is such a year --
+   and the primary-source scan available to this project does not contain an
+   explicit numbered-paragraph statement of either rule (searched; see
+   register §3 "Ember days"), so this citation is deliberately left at the
+   rank rules only (RG 91 entries 18/22, cited on [ember] below), not the
+   date-derivation rule itself: a wrong citation is worse than none.
+   Empirically: for 2025 this rule gives 24/26/27 September, confirmed
+   against an independent oracle; the Holy-Cross rule would give 17/19/20
+   September instead. See register §3 for the full note. *)
 let third_sunday_of_september y =
   let sep1 = mk y 9 1 in
   let first_sunday = Date.add_days sep1 ((7 - weekday_index sep1) mod 7) in
@@ -215,7 +273,13 @@ let third_sunday_of_september y =
 (* Ember days: Wednesday, Friday and Saturday after the anchoring Sunday.
    RG 91 entry 18 makes the Advent, Lent and September sets II class; entry 22
    excepts the Lenten set from the III-class Lenten ferias. The Whitsun set
-   falls inside the I-class Pentecost octave and takes its rank. *)
+   falls inside the I-class Pentecost octave and takes its rank.
+
+   The September and Advent sets match lectio's own Ember slugs. The Lent and
+   Whitsun (Pentecost) sets do not -- lectio has no Ember slug for either, so
+   "ef-lent-ember-*" and "ef-pentecost-ember-*" are colitur-only keys and a
+   lectionary gap for the Plan 3 bootstrap to fill (spec §4.4), the same
+   status as the Nativity vigil and the Rogation days below. *)
 let ember d =
   let y = Date.year d in
   let easter = Computus.gregorian_easter y in
@@ -249,12 +313,19 @@ let privileged_feria d =
   let n = days_between easter d in
   (n >= -6 && n <= -1) || (n >= 1 && n <= 6) || (n >= 50 && n <= 55)
 
+(* RG 117 enumerates the five colours (white, red, green, violet, black);
+   RG 127 assigns green and RG 128 violet to the seasons de Tempore below.
+   White's own specific paragraph (the "B) De colore albo" section, between
+   117 and 123) was not pinned by the primary-source search available here --
+   left uncited rather than guessed; see register §3 "Colours". *)
 let season_colour = function
-  | Advent | Septuagesima | Lent | Passiontide -> Colour.Violet
+  | Advent | Septuagesima | Lent | Passiontide -> Colour.Violet (* RG 128 *)
   | Christmastide | Paschaltide -> Colour.White
-  | Time_after_epiphany | Time_after_pentecost -> Colour.Green
+  | Time_after_epiphany | Time_after_pentecost -> Colour.Green (* RG 127 *)
 
-(* Gaudete (Advent III) and Laetare (Lent IV) are rose. *)
+(* Gaudete (Advent III) and Laetare (Lent IV) are rose: RG 131, "may be used...
+   for the Office and Mass of that Sunday only" -- an indult over the
+   season's violet, not a season colour of its own. *)
 let is_rose_sunday d s =
   let y = Date.year d in
   match s with
@@ -290,14 +361,20 @@ let temporal d =
     { Colitur_kernel.Temporal.season; week; weekday; office }
   in
   match named d with
-  | Some (season, slug, colour, rank, week) -> build ~season ~slug ~colour ~rank ~week
+  | Some (season, slug, colour, rank) -> build ~season ~slug ~colour ~rank ~week:(week d)
   | None -> (
-      (* Rogations: RG 80/87, Monday and Tuesday before Ascension. The
-         Wednesday is the Ascension vigil (see Task 11). RG 88: "de Litaniis
-         minoribus nihil fit in Officio" -- the Office (hence the day's rank)
-         is unchanged by the Rogation; only the Mass is proper. No RG 91 table
-         entry elevates these days, so they take the ordinary ferial rank of
-         their season via [ferial_rank] rather than a fixed class. *)
+      (* Rogations (the Minor Litanies only -- RG 87, Monday and Tuesday
+         before Ascension). The Major Litanies (25 April, RG 80) are a fixed
+         date and are not yet computed; they arrive with Plan 3's sanctoral
+         (register §6). The Wednesday here is the Ascension vigil (see Task
+         11). RG 88: "de Litaniis minoribus nihil fit in Officio" -- the
+         Office (hence the day's rank) is unchanged by the Rogation; only the
+         Mass is proper. No RG 91 table entry elevates these days, so they
+         take the ordinary ferial rank of their season via [ferial_rank]
+         rather than a fixed class. lectio has no Rogation slug at all, so
+         "ef-rogation-monday"/"-tuesday" are colitur-only keys and a
+         lectionary gap for Plan 3, like the Ember and Nativity-vigil keys
+         above. *)
       let rogation = days_between easter d in
       if rogation = 36 || rogation = 37 then
         build ~season:s
@@ -312,30 +389,66 @@ let temporal d =
                 let colour = if is_rose_sunday d s then Colour.Rose else season_colour s in
                 (* RG 11-12: Sundays of Advent, Lent, Passiontide, Easter, Low
                    Sunday and Pentecost are I class; all others II. The I-class
-                   ones are already named above, so anything reaching here is
-                   II class except the remaining Advent and Lent Sundays. *)
-                let rank = match s with Advent | Lent | Passiontide -> Class1 | _ -> Class2 in
+                   ones are already named above -- Passiontide has only two
+                   Sundays and both are named, so no Passiontide Sunday ever
+                   reaches this fallback -- leaving II class here except the
+                   remaining Advent and Lent Sundays. *)
+                let rank = match s with Advent | Lent -> Class1 | _ -> Class2 in
                 build ~season:s ~slug ~colour ~rank ~week:(week d)
-            | None ->
-                (* The days between Ash Wednesday and Lent I have proper Masses
-                   and belong to no numbered week. *)
-                let after_ashes = days_between easter d in
-                if after_ashes >= -45 && after_ashes <= -43 then
-                  build ~season:s
-                    ~slug:(Printf.sprintf "ef-lent-after-ashes-%s" (weekday_word d))
-                    ~colour:Colour.Violet ~rank:Class3 ~week:None
-                else
-                  let colour =
-                    (* The Pentecost octave weekdays are red, not Paschaltide's white. *)
-                    if days_between easter d >= 50 && days_between easter d <= 55 then Colour.Red
-                    else season_colour s
-                  in
-                  let week_n = week d in
-                  let slug =
-                    Printf.sprintf "ef-%s-%d-%s" (season_slug_word s)
-                      (Option.value week_n ~default:0) (weekday_word d)
-                  in
-                  build ~season:s ~slug ~colour ~rank:(ferial_rank d s) ~week:week_n))
+            | None -> (
+                match christmastide_feria_slug d with
+                | Some slug ->
+                    build ~season:s ~slug ~colour:(season_colour s) ~rank:(ferial_rank d s) ~week:(week d)
+                | None ->
+                    (* The days between Ash Wednesday and Lent I have proper
+                       Masses and belong to no numbered week. *)
+                    let after_ashes = days_between easter d in
+                    if after_ashes >= -45 && after_ashes <= -43 then
+                      build ~season:s
+                        ~slug:(Printf.sprintf "ef-lent-after-ashes-%s" (weekday_word d))
+                        ~colour:Colour.Violet ~rank:Class3 ~week:None
+                    else
+                      let colour =
+                        (* The Pentecost octave weekdays are red, not Paschaltide's white. *)
+                        if days_between easter d >= 50 && days_between easter d <= 55 then Colour.Red
+                        else season_colour s
+                      in
+                      let week_n = week d in
+                      let slug =
+                        Printf.sprintf "ef-%s-%d-%s" (season_slug_word s)
+                          (Option.value week_n ~default:0) (weekday_word d)
+                      in
+                      build ~season:s ~slug ~colour ~rank:(ferial_rank d s) ~week:week_n)))
+
+(* Independent restatement of [named]'s fixed and Easter-relative dates,
+   paired with the slug each should carry, for civil year [y]. Deliberately
+   NOT derived from [named] itself -- consumed by [Validate]'s anchor-
+   agreement check (design spec §5.7), which exists precisely to catch an
+   accidental single-site drift (e.g. Ascension's [off 39] silently becoming
+   [off 40]) that both sides moving together would hide. *)
+let anchors y =
+  let easter = Computus.gregorian_easter y in
+  let off n = Date.add_days easter n in
+  [ ("ef-nativity", mk y 12 25);
+    ("ef-nativity-vigil", mk y 12 24);
+    ("ef-nativity-octave-day-5", mk y 12 29);
+    ("ef-nativity-octave-day-6", mk y 12 30);
+    ("ef-nativity-octave-day-7", mk y 12 31);
+    ("ef-circumcision", mk y 1 1);
+    ("ef-epiphany", mk y 1 6);
+    ("ef-ash-wednesday", off (-46));
+    ("ef-passion-sunday", off (-14));
+    ("ef-palm-sunday", off (-7));
+    ("ef-easter-sunday", off 0);
+    ("ef-low-sunday", off 7);
+    ("ef-ascension-vigil", off 38);
+    ("ef-ascension", off 39);
+    ("ef-pentecost-vigil", off 48);
+    ("ef-pentecost", off 49);
+    ("ef-trinity", off 56);
+    ("ef-corpus-christi", off 60);
+    ("ef-sacred-heart", off 68);
+    ("ef-christ-the-king", christ_the_king y) ]
 
 (* Compile-time check that this module satisfies the kernel's rite contract. *)
 module _ : Colitur_kernel.Temporal.RITE = struct