Merge branch 'ef-plan3': Plan 3, the EF resolution engine

Adds the rite-parameterised Precedence resolver, Liturgical_day, Rite,
and Calendar (year as the primitive, because transfers need whole-year
knowledge), the full EF precedence ruleset (RG 91's 28-entry table,
occurrence RG 92-95, commemorations RG 108-111, transfers RG 96-98),
322 bootstrapped sanctoral entries, colitur day <year>, and validation
layers 3-5.

Layer 3 diffs 16801 days against lectio; layer 4 diffs 730 days against
missalemeum; layer 5 pins ~30 dates on the known-tricky years. Both
comparison layers carry cited allow-lists that name the governing RG
paragraph and which engine is right.

The oracle layer earned its place immediately: Holy Thursday was violet
in colitur and lectio alike, because colitur's data was bootstrapped
from lectio and both carried the same error. Only an independent source
could see it. RG 128(b) and RG 122 name it white.

1 files changed, 437 insertions, 11 deletions

diff --git a/test/test_validate.ml b/test/test_validate.ml
index c19957d..89053c1 100644
--- a/test/test_validate.ml
+++ b/test/test_validate.ml
@@ -1,9 +1,40 @@
 module Val = Colitur_kernel.Validate
+module Rite = Colitur_kernel.Rite
+module P = Colitur_kernel.Precedence
+module Layer = Colitur_kernel.Layer
+module Overlay = Colitur_kernel.Overlay
 module V = Rite_ef.Vocab_ef
 module T = Rite_ef.Temporal_ef
 
-let run year =
-  Val.run V.vocab ~year_start:T.year_start ~temporal:T.temporal ~anchors:T.anchors ~year
+(* Task 12 widens Validate.run to take a resolved layer -- Precedence_ef and
+   Calendar (Tasks 5-11) now exist, so the REAL EF rite (Rite_ef.context) and
+   its REAL bootstrapped data replace the earlier placeholder rules/layer-less
+   Rite.t this module used before Plan 3's resolution engine was built.
+   Relative to this test's own build directory (_build/default/test/), same
+   convention test_rite_ef.ml already uses -- test/dune declares both as deps
+   of the (test ...) stanza. *)
+let sanctoral_path = "../data/ef/sanctoral.sexp"
+let adjustments_path = "../data/ef/adjustments.sexp"
+
+(* Loaded once at module init, not per call: [run] below is called by every
+   test and by the 200-sample property, and Calendar.year's own resolution
+   cost already dominates -- there is no reason to also re-parse a 322-entry
+   sexp file on every one of those calls. *)
+let real_ef_layer =
+  match Layer.load V.rank_of_sexp sanctoral_path with
+  | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" sanctoral_path e)
+  | Ok layer -> (
+      match Overlay.load V.rank_of_sexp adjustments_path with
+      | Error e -> failwith (Printf.sprintf "%s: failed to load: %s" adjustments_path e)
+      | Ok overlay ->
+          let layer, diagnostics = Overlay.apply layer overlay in
+          if diagnostics <> [] then
+            failwith
+              (Printf.sprintf "unexpected overlay diagnostics: %s"
+                 (String.concat "; " (List.map Overlay.diagnostic_to_string diagnostics)));
+          layer)
+
+let run year = Val.run Rite_ef.context real_ef_layer ~year
 
 let check_year year =
   match run year with
@@ -46,10 +77,18 @@ let extreme_years () =
 
 let test_easter_extremes () =
   let ys = extreme_years () in
-  (* Both extremes genuinely occur in 1583..2500 (earliest 1818, latest
-     2038); requiring just "non-empty" would have passed even if the search
-     silently found only one of them (register finding 15). *)
-  Alcotest.(check int) "found both extreme years (earliest 22 Mar and latest 25 Apr)" 2 (List.length ys);
+  (* Both extremes genuinely occur in 1583..2500 (earliest 1598, latest
+     1666 -- verified against Computus.gregorian_easter directly, not
+     transcribed). CORRECTED (final fix wave, item 7): this used to assert
+     only [List.length ys = 2], a cardinality check where an identity check
+     was called for -- the comment already named 1598 and 1666, but nothing
+     confirmed [ys] actually contained THOSE two years rather than some
+     other pair the search happened to find first; a version of
+     [extreme_years] that silently found the wrong two years but still
+     found exactly two would have passed this unchanged. Asserting the
+     identities directly is strictly stronger and costs nothing extra. *)
+  Alcotest.(check (list int)) "found exactly 1598 (earliest 22 Mar) and 1666 (latest 25 Apr)"
+    [ 1598; 1666 ] ys;
   List.iter check_year ys
 
 (* The confidence-to-9999 core: random years across the whole domain. *)
@@ -58,6 +97,74 @@ let prop_invariants =
     (QCheck.int_range 1583 9998)
     (fun y -> run y = [])
 
+(* ---- final fix wave, item 6: the exhaustive sweep, committed ----
+
+   The property above samples 200 of 8 416 years (2.4% of the domain) on a
+   RANDOM seed -- QCheck.Test.make with no ~seed argument draws a fresh one
+   from the environment/OS entropy each run, and two consecutive runs of
+   this suite were observed using different seeds (see the task report for
+   the transcript). CLAUDE.md's standing claim that Validate is "clean
+   across all 8 416 years -- exhaustive, not sampled" was true whenever it
+   was last actually re-run in full, but no committed artifact pinned it,
+   and a year-specific regression (one bad year among 8 416) would show up
+   in this suite only intermittently -- roughly 200/8416 of the time per
+   run, i.e. most runs would NOT catch it.
+
+   This is that committed artifact: every year 1583..9999, not a sample.
+   Tagged `Slow (matching this file's own naming for the check it performs
+   -- see [suite] below), but Alcotest's speed-level filtering is deliberately
+   NOT used to keep it out of the default `dune test`: that filtering (the
+   `-q`/`--quick-tests` flag, or dune wiring the runtest action to pass it)
+   is ALL-OR-NOTHING per speed level, and this codebase already tags SIX
+   OTHER cases `Slow -- the two pre-existing exhaustive Computus checks
+   (test_computus.ml, both genuinely fast, sub-second) AND, found while
+   implementing this item, EVERY QCheck property in the whole suite
+   (test_date.ml x3, test_overlay.ml, test_temporal_ef.ml, and
+   [prop_invariants] immediately above, since QCheck_alcotest.to_alcotest
+   defaults ~speed_level to `Slow when not given explicitly, which none of
+   this codebase's call sites do). Wiring `-q` at the dune level was tried
+   and reverted: it made the default `dune test` report 251 tests instead
+   of (the then-current) 260, silently excluding [prop_invariants] itself
+   -- the "confidence-to-9999" mechanism CLAUDE.md documents as this
+   project's central property-testing story -- along with five other
+   properties, none of which this task asked to remove from the fast path.
+   That is a far bigger, unintended regression than the one line this item
+   asks to add.
+
+   Instead, this test gates its OWN expensive body on an environment
+   variable, [COLITUR_EXHAUSTIVE_SWEEP], and calls {!Alcotest.skip} (marked
+   SKIPPED, not silently passed, when unset) so `dune test`'s default run
+   stays at its normal speed and reports the skip honestly rather than a
+   vacuous green. To run the real sweep (~35-45s, see the report for the
+   measured figure):
+
+     COLITUR_EXHAUSTIVE_SWEEP=1 dune test --force
+
+   or invoke the built executable directly with the same variable set. *)
+let colitur_exhaustive_sweep_env = "COLITUR_EXHAUSTIVE_SWEEP"
+
+(* 9999 is a documented, non-regression truncation, not a fresh finding:
+   [test_year_9999_does_not_raise] above already pins that [run 9999]
+   reports exactly a "seasons" failure (the domain's own ceiling truncates
+   the scan mid-Christmastide) and nothing else -- reused here rather than
+   calling [check_year] on 9999, which would fail this sweep on a shape
+   that is not a regression. *)
+let test_exhaustive_domain_sweep () =
+  if Sys.getenv_opt colitur_exhaustive_sweep_env = None then Alcotest.skip ()
+  else begin
+    for y = 1583 to 9998 do
+      check_year y
+    done;
+    let fs = run 9999 in
+    Alcotest.(check bool) "9999: no coverage failures (temporal stayed total through the clamp)" true
+      (not (List.exists (fun f -> f.Val.check = "coverage") fs));
+    Alcotest.(check bool) "9999: seasons check flags the truncated final year as incomplete" true
+      (List.exists (fun f -> f.Val.check = "seasons") fs);
+    Alcotest.(check (list string)) "9999: nothing OTHER than the documented seasons truncation fired"
+      [ "seasons" ]
+      (List.sort_uniq compare (List.map (fun f -> f.Val.check) fs))
+  end
+
 (* ---- negative-path fixture (Task 14 review, finding 1) ----
 
    Everything above only exercises the CLEAN path against real EF data: an
@@ -77,6 +184,10 @@ module Synthetic = struct
   module Slug = Colitur_kernel.Slug
   module Colour = Colitur_kernel.Colour
   module Temporal = Colitur_kernel.Temporal
+  module P = Colitur_kernel.Precedence
+  module Rite = Colitur_kernel.Rite
+  module Layer = Colitur_kernel.Layer
+  module Date_spec = Colitur_kernel.Date_spec
 
   type season = A | B
   type rank = R1 | R2
@@ -105,6 +216,17 @@ module Synthetic = struct
   let vocab_collapsed_ranks = { vocab with Vocab.rank_to_string = (fun _ -> "same") }
   let vocab_collapsed_seasons = { vocab with Vocab.season_to_string = (fun _ -> "same") }
 
+  (* The placeholder ruleset every TEMPORAL-only fixture below still uses:
+     paired with the default empty [layer] (see [rite] below), there is never
+     a sanctoral candidate for these three functions to be called against, so
+     what they return is moot for those tests -- only the Task 12 resolution
+     fixtures further down override [rules] (and supply a non-empty
+     [layer]), each with its own small, deliberately-shaped ruleset. *)
+  let rules : (season, rank) P.rules =
+    { P.band = (fun _ _ -> 0);
+      disposition = (fun ~winner:_ ~loser:_ -> P.Omit);
+      admit = (fun ~observed:_ _ -> []) }
+
   let year_start y = match D.make ~year:y ~month:1 ~day:1 with Ok d -> d | Error e -> failwith e
 
   let weekday_index d =
@@ -149,10 +271,228 @@ module Synthetic = struct
      this synthetic rite too, not only in EF. *)
   let anchors _y = [ (Slug.to_string (good target).Temporal.office.Cel.slug, target) ]
 
-  let run ?(vocab = vocab) ?(anchors = fun _ -> []) temporal =
-    Val.run vocab ~year_start ~temporal ~anchors ~year:2026
+  (* Task 12: [rite] now also takes [rules]/[transfer_target] (defaulting to
+     the placeholder above and to "stand still", respectively -- harmless
+     defaults against the default empty [layer], since nothing ever contests
+     the temporal office there) so the resolution fixtures further down can
+     override them without duplicating every other field. *)
+  let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules)
+      ?(transfer_target = fun _ origin _ -> origin) temporal : (season, rank) Rite.t =
+    { Rite.id = "synthetic"; vocab; year_start; temporal; anchors; rules; season_runs;
+      transfer_target }
+
+  (* Empty by default: every check built before Task 12 exercises the
+     TEMPORAL-only pass, where an empty layer is exactly the fixture that
+     leaves it unable to affect anything ([Precedence.resolve] against no
+     sanctoral candidates always just observes the temporal office
+     unchallenged). Task 12's own resolution fixtures pass their own. *)
+  let empty_layer = Layer.empty ~id:"synthetic-empty" ~name:"empty"
+
+  let run ?vocab ?anchors ?season_runs ?rules ?transfer_target ?(layer = empty_layer) temporal =
+    Val.run (rite ?vocab ?anchors ?season_runs ?rules ?transfer_target temporal) layer ~year:2026
 
   let has_check check (fs : Val.failure list) = List.exists (fun f -> f.Val.check = check) fs
+
+  (* A rite whose season B legitimately appears in two separate runs: the
+     civil year is split into calendar quarters, seasons alternating A B A B
+     -- as the modern form's Ordinary Time does (January-Ash Wednesday, then
+     Pentecost-Advent, with Lent/Easter and Advent/Christmas between). Each
+     quarter gets its own Sunday-aligned week origin, exactly as [good] does
+     for its own two runs, so every other invariant (weekday, week
+     numbering, rank, colour, determinism) stays clean and only the season
+     check is actually exercised. *)
+  let quarter_start y i =
+    match D.make ~year:y ~month:(1 + (i * 3)) ~day:1 with Ok d -> d | Error e -> failwith e
+
+  let quarter_index d = (D.month d - 1) / 3
+
+  let two_run_temporal d =
+    let y = D.year d in
+    let qi = quarter_index d in
+    let s = if qi mod 2 = 0 then A else B in
+    let origin = sunday_on_or_before (quarter_start y qi) in
+    let n = floor_div (D.to_rata d - D.to_rata origin) 7 + 1 in
+    let slug = Printf.sprintf "syn2-%s-%d" (season_to_string s) (D.to_rata d) in
+    let rank = if D.weekday d = D.Sun then R1 else R2 in
+    { Temporal.season = s; week = Some n; weekday = D.weekday d;
+      office = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.Green ~layer:"synthetic" () }
+
+  let rite_with_two_runs : (season, rank) Rite.t =
+    rite ~season_runs:[ A; B; A; B ] two_run_temporal
+
+  (* ---- Task 12: resolution-level fixtures ----
+
+     Everything above only ever drives the TEMPORAL-only pass: [run]'s
+     default [layer] is empty, so [Precedence.resolve] never has a sanctoral
+     candidate to contest against the temporal office, and [rules]/
+     [transfer_target] are never meaningfully exercised. These five fixtures
+     instead give [Calendar.year] real work -- a non-empty [layer] plus a
+     small, deliberately-shaped [rules] (and, for two of them,
+     [transfer_target]) -- each built so its OWN check label fires. Four of
+     the five fire in clean isolation (the other four Task 12 labels stay
+     silent); the fifth (["unconverged"]) genuinely also fires
+     ["duplicated"] alongside it, a real consequence of Calendar's own round-
+     guard accounting, not a fixture design flaw -- see guard_rules's own
+     comment. Every fixture's isolation (or lack of it) was verified by
+     hand-tracing [Calendar]'s resolution mechanics BEFORE writing its
+     assertion (see the task report), not inferred from what the assertion
+     happens to require -- the tests below check that trace against the
+     actual engine output, one fixture at a time. [good] is reused,
+     unchanged, as every fixture's [temporal]: only [rules]/[layer]/
+     [transfer_target] vary, so the temporal-only checks (already proven
+     clean against [good] by [test_synthetic_baseline_is_clean]) cannot be
+     what fires here. *)
+
+  let mk_entry ~month ~day ~slug ~rank =
+    { Layer.date = (match Date_spec.fixed ~month ~day with Ok d -> d | Error e -> failwith e);
+      cel = Cel.make ~slug:(Slug.of_string_exn slug) ~rank ~colour:Colour.White
+              ~layer:"synthetic-sanctoral" () }
+
+  let task12_checks = [ "observed"; "lost"; "duplicated"; "unconverged"; "admission" ]
+
+  (* The Task-12-owned subset of a failure list's own check labels, as a
+     sorted, de-duplicated set -- what each isolation assertion below
+     compares against, so a fixture that (by mistake) also trips an
+     unrelated Task-12 check shows up as a wrong set, not a silently-passing
+     [has_check]. *)
+  let fired_task12_checks (fs : Val.failure list) =
+    List.filter_map (fun f -> if List.mem f.Val.check task12_checks then Some f.Val.check else None) fs
+    |> List.sort_uniq compare
+
+  (* "duplicated": a single ordinary sanctoral entry, always losing to the
+     temporal office (band: Temporal 0 < Sanctoral 10, unconditionally) and
+     always Commemorate-disposed. [admit]'s bug is exactly the shape
+     precedence_ef.mli's own [admit] contract warns against ("a value taken
+     unchanged from comms, never rebuilt"): it REBUILDS every admitted pair
+     via a record update, allocating a fresh, structurally-identical-but-
+     physically-distinct candidate. Precedence.resolve's own [dropped]
+     computation tells an admitted candidate from a dropped one by PHYSICAL
+     equality, so the rebuild defeats it -- the one candidate ends up counted
+     as both admitted (in [commemorations]) and dropped (in [omitted],
+     "admission limit reached"): two sightings for one Date_spec
+     resolution. *)
+  let dup_entry = mk_entry ~month:5 ~day:5 ~slug:"dup-target" ~rank:R2
+  let dup_layer = Layer.of_entries ~id:"dup" ~name:"dup" [ dup_entry ]
+
+  let dup_rules : (season, rank) P.rules =
+    { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
+      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
+      admit = (fun ~observed:_ cs -> List.map (fun (c, p) -> ({ c with P.origin = c.P.origin }, p)) cs) }
+
+  (* "unconverged": two entries collide on one date (6 June), both beating
+     the temporal office and tied with each other, so slug decides:
+     "guard-aaa" wins the day outright every time, "guard-zzz" is always the
+     loser there and always Transfer-disposed. Paired with a
+     [transfer_target] that always answers with the impeded day itself --
+     never strictly forward -- this is the exact non-terminating shape
+     test_calendar.ml's own
+     [test_transfer_guard_records_failure_instead_of_looping] proves hits
+     Calendar's round guard: "guard-zzz", re-injected into 6 June every
+     round, can never win it (it always loses the tie to the natural
+     "guard-aaa" copy already sitting there), so [deferred] never empties.
+
+     GENUINE FINDING (see the task report): this ALSO fires "duplicated", not
+     "unconverged" alone. Once the guard is hit, [build_day]'s final resolve
+     at 6 June sees "guard-zzz" TWICE -- once as the permanent natural entry
+     (which never stops losing there) and once as whatever the last round's
+     [injected] state still holds for it -- and [unresolved] is evaluated per
+     CANDIDATE OBJECT, not per slug, so BOTH copies land in [omitted] with
+     the unconverged reason. Nothing is lost (both copies carry a recorded
+     reason), but the slug is sighted twice against one Date_spec resolution,
+     which is exactly what "duplicated" is for. The same double-recording is
+     latent in test_calendar.ml's own guard fixture too (day_winner/eclipsed
+     at 20 Dec, structurally identical) -- untested there only because that
+     test uses [List.exists], not a count. Calendar's round guard is
+     documented as "nothing in the 1962 calendar is expected to trigger"
+     (calendar.ml), so this is a latent accounting quirk in an unreachable
+     path, not a live bug, and calendar.ml is out of this task's file list --
+     reported, not fixed here. *)
+  let guard_winner_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-aaa" ~rank:R1
+  let guard_loser_entry = mk_entry ~month:6 ~day:6 ~slug:"guard-zzz" ~rank:R1
+  let guard_layer = Layer.of_entries ~id:"guard" ~name:"guard" [ guard_winner_entry; guard_loser_entry ]
+
+  let guard_rules : (season, rank) P.rules =
+    { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 50 | P.Sanctoral -> 10);
+      disposition =
+        (fun ~winner:_ ~loser ->
+          match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary);
+      admit = (fun ~observed:_ cs -> cs) }
+
+  let guard_transfer_target (_ : rank P.candidate) (origin : D.t) (_ : D.t -> rank Cel.t) = origin
+
+  (* "admission": three entries collide on one date (9 September), all
+     losing to the temporal office (band: Temporal 0 < Sanctoral 10) and all
+     Commemorate-disposed -- a genuine 3-candidate offer to [admit]. The bug:
+     cap 2 when the offer's length is ODD, cap 1 when EVEN -- a length-keyed
+     rule with no liturgical meaning, chosen as the simplest function that is
+     NOT idempotent on its own output (offer 3, admit 2; re-offer those same
+     2, admit only 1) while staying idempotent -- and so invisible -- on
+     every OTHER shape this suite exercises (never offered exactly 2 or 3
+     candidates elsewhere), including its own clean 3-candidate day. *)
+  let adm_a_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-a" ~rank:R2
+  let adm_b_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-b" ~rank:R2
+  let adm_c_entry = mk_entry ~month:9 ~day:9 ~slug:"adm-c" ~rank:R2
+  let adm_layer = Layer.of_entries ~id:"adm" ~name:"adm" [ adm_a_entry; adm_b_entry; adm_c_entry ]
+
+  let adm_compare_slug (c1, _) (c2, _) = Slug.compare c1.P.cel.Cel.slug c2.P.cel.Cel.slug
+
+  let rec adm_take n = function
+    | [] -> []
+    | x :: xs -> if n <= 0 then [] else x :: adm_take (n - 1) xs
+
+  let adm_rules : (season, rank) P.rules =
+    { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
+      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
+      admit =
+        (fun ~observed:_ cs ->
+          let sorted = List.stable_sort adm_compare_slug cs in
+          if List.length sorted mod 2 = 1 then adm_take 2 sorted else adm_take 1 sorted) }
+
+  (* "observed": two DIFFERENT layer entries sharing one slug -- a realistic
+     data mistake (a renamed or duplicated entry), not prevented by
+     [Layer.t]'s own type. [collide_a] (1 Feb, rank R1) always loses on its
+     OWN date: [band] makes the temporal office win there specifically (5,
+     beating R1's 10) and lose everywhere else (50), so [collide_a] is always
+     Transfer-disposed at 1 Feb. Its constant [transfer_target] sends it to
+     10 Feb -- [collide_b]'s own home date -- where [collide_a]'s rank R1
+     (band 10) now beats both the temporal office (50, since the date is no
+     longer 1 Feb) and [collide_b]'s own rank R2 (band 90): the ARRIVING
+     [collide_a] wins 10 Feb outright, and [collide_b] -- same slug as the
+     new winner -- is Commemorate-disposed (R2) right alongside it. One day
+     ends up reporting the same slug as both its observed celebration and one
+     of its own commemorations. *)
+  let collide_d1 = match D.make ~year:2026 ~month:2 ~day:1 with Ok d -> d | Error e -> failwith e
+  let collide_a_entry = mk_entry ~month:2 ~day:1 ~slug:"collide-x" ~rank:R1
+  let collide_b_entry = mk_entry ~month:2 ~day:10 ~slug:"collide-x" ~rank:R2
+  let collide_layer = Layer.of_entries ~id:"collide" ~name:"collide" [ collide_a_entry; collide_b_entry ]
+
+  let collide_rules : (season, rank) P.rules =
+    { P.band =
+        (fun ctx c ->
+          match c.P.origin with
+          | P.Temporal -> if D.compare ctx.P.date collide_d1 = 0 then 5 else 50
+          | P.Sanctoral -> ( match c.P.cel.Cel.rank with R1 -> 10 | R2 -> 90));
+      disposition =
+        (fun ~winner:_ ~loser ->
+          match loser.P.cel.Cel.rank with R1 -> P.Transfer | R2 -> P.Commemorate P.Ordinary);
+      admit = (fun ~observed:_ cs -> cs) }
+
+  let collide_d2 = match D.make ~year:2026 ~month:2 ~day:10 with Ok d -> d | Error e -> failwith e
+  let collide_transfer_target (_ : rank P.candidate) (_ : D.t) (_ : D.t -> rank Cel.t) = collide_d2
+
+  (* A genuinely resolved, well-behaved day (one ordinary sanctoral entry,
+     cleanly losing and commemorated, nothing transferred) -- proving the
+     five checks stay silent against REAL resolution machinery, not merely
+     against the default empty [layer] every fixture above this section
+     uses. Without this, "no check fires" would only ever have been shown
+     for a layer with nothing in it. *)
+  let clean_sanctoral_entry = mk_entry ~month:8 ~day:8 ~slug:"clean-saint" ~rank:R2
+  let clean_sanctoral_layer = Layer.of_entries ~id:"clean" ~name:"clean" [ clean_sanctoral_entry ]
+
+  let clean_sanctoral_rules : (season, rank) P.rules =
+    { P.band = (fun _ c -> match c.P.origin with P.Temporal -> 0 | P.Sanctoral -> 10);
+      disposition = (fun ~winner:_ ~loser:_ -> P.Commemorate P.Ordinary);
+      admit = (fun ~observed:_ cs -> cs) }
 end
 
 open Synthetic
@@ -160,6 +500,18 @@ open Synthetic
 let test_synthetic_baseline_is_clean () =
   Alcotest.(check bool) "clean synthetic fixture has no failures" true (run good = [])
 
+(* The point of this task: a rite whose season B genuinely appears in two
+   separate runs (quarters 0,1,2,3 give season sequence A B A B, not a single
+   A-then-B pair) validates clean when [season_runs] says so. Before this
+   task, [Validate]'s season check hardcoded "compressed = vocab.seasons"
+   ([A; B]) with no way to say otherwise -- against that check this fixture's
+   compressed sequence, [A; B; A; B], would never match and every year would
+   report a spurious "seasons" failure. *)
+let test_two_run_season_is_accepted () =
+  let r = Synthetic.rite_with_two_runs in
+  Alcotest.(check (list string)) "no failures" []
+    (List.map Val.failure_to_string (Val.run r Synthetic.empty_layer ~year:2026))
+
 let test_coverage_fires () =
   let temporal d = if D.compare d target = 0 then failwith "boom" else good d in
   Alcotest.(check bool) "coverage check fires when temporal raises" true
@@ -170,10 +522,10 @@ let test_seasons_fires () =
     let t = good d in
     let y = D.year d in
     let flip_after = match D.make ~year:y ~month:9 ~day:1 with Ok d -> d | Error e -> failwith e in
-    (* Season A reappears after B: breaks "each season, one unbroken run". *)
+    (* Season A reappears after B: breaks the expected [A; B] run sequence. *)
     if D.compare d flip_after >= 0 then { t with Temporal.season = A } else t
   in
-  Alcotest.(check bool) "seasons check fires when a season recurs" true
+  Alcotest.(check bool) "seasons check fires when a season recurs outside season_runs" true
     (has_check "seasons" (run temporal))
 
 let test_week_fires () =
@@ -263,12 +615,76 @@ let test_vocab_season_injectivity_fires () =
   Alcotest.(check bool) "vocab check fires when season_to_string collapses two seasons to one string" true
     (has_check "vocab" (run ~vocab:vocab_collapsed_seasons good))
 
+(* Plan 2 carried item 4: slug uniqueness moves into [Validate] itself, no
+   exemption. [target] (17 March, mid-run) is given the NEXT day's real slug
+   verbatim -- a genuine collision between two distinct dates in the same
+   walked year, touching only the [slug] field so every other check (season,
+   week, weekday, rank, colour, determinism, anchor) stays silent against it. *)
+let test_slugs_fires () =
+  let colliding_slug = (good (D.add_days target 1)).Temporal.office.Cel.slug in
+  let temporal d =
+    let t = good d in
+    if D.compare d target = 0 then
+      { t with Temporal.office = { t.Temporal.office with Cel.slug = colliding_slug } }
+    else t
+  in
+  Alcotest.(check bool) "slugs check fires when two dates in the year share a slug" true
+    (has_check "slugs" (run temporal))
+
+(* ---- Task 12: resolution invariants ----
+
+   Each test below asserts that exactly one of the five new check labels
+   fires for its own dedicated fixture (Synthetic's own comments carry the
+   hand-traced mechanics) -- not merely "at least this one", so a fixture
+   that turns out to also trip an unrelated Task 12 check would fail loudly
+   here rather than reading as accidental corroboration. *)
+
+let test_lost_fires_on_resolution_exception () =
+  (* Reuses [test_coverage_fires]'s own broken [temporal]: [Calendar.year]
+     calls [rite.temporal] with no exception guard of its own (unlike the
+     temporal-only pass above, which wraps every call), so the same raise
+     that trips "coverage" also makes resolution itself raise -- the most
+     total form of "silently lost" there is, per validate.mli. *)
+  let temporal d = if D.compare d target = 0 then failwith "boom" else good d in
+  Alcotest.(check (list string)) "only the lost check fires" [ "lost" ] (fired_task12_checks (run temporal))
+
+let test_duplicated_fires () =
+  Alcotest.(check (list string)) "only the duplicated check fires" [ "duplicated" ]
+    (fired_task12_checks (run ~layer:dup_layer ~rules:dup_rules good))
+
+let test_unconverged_fires () =
+  (* Also asserts "duplicated" fires alongside it -- see guard_rules's own
+     comment for why that is the genuine, hand-verified consequence of
+     hitting the round guard here, not an isolation failure. *)
+  Alcotest.(check (list string)) "unconverged fires, and duplicated alongside it"
+    [ "duplicated"; "unconverged" ]
+    (fired_task12_checks
+       (run ~layer:guard_layer ~rules:guard_rules ~transfer_target:guard_transfer_target good))
+
+let test_admission_fires () =
+  Alcotest.(check (list string)) "only the admission check fires" [ "admission" ]
+    (fired_task12_checks (run ~layer:adm_layer ~rules:adm_rules good))
+
+let test_observed_fires () =
+  Alcotest.(check (list string)) "only the observed check fires" [ "observed" ]
+    (fired_task12_checks
+       (run ~layer:collide_layer ~rules:collide_rules ~transfer_target:collide_transfer_target good))
+
+(* The positive counterpart: a genuinely resolved, well-behaved day (real
+   sanctoral entry, real contest, real commemoration) must report none of the
+   five checks -- proven against actual resolution machinery, not only
+   against every OTHER fixture's default empty layer. *)
+let test_resolution_checks_clean_on_a_well_behaved_layer () =
+  Alcotest.(check (list string)) "none of the five checks fire" []
+    (fired_task12_checks (run ~layer:clean_sanctoral_layer ~rules:clean_sanctoral_rules good))
+
 let suite =
   ( "Validate",
     [ Alcotest.test_case "landmark years" `Quick test_landmark_years;
       Alcotest.test_case "year 9999 does not raise" `Quick test_year_9999_does_not_raise;
       Alcotest.test_case "easter extremes" `Quick test_easter_extremes;
       Alcotest.test_case "synthetic baseline is clean" `Quick test_synthetic_baseline_is_clean;
+      Alcotest.test_case "two-run season is accepted" `Quick test_two_run_season_is_accepted;
       Alcotest.test_case "coverage fires" `Quick test_coverage_fires;
       Alcotest.test_case "seasons fires" `Quick test_seasons_fires;
       Alcotest.test_case "week fires" `Quick test_week_fires;
@@ -279,5 +695,15 @@ let suite =
       Alcotest.test_case "anchor clean" `Quick test_anchor_clean;
       Alcotest.test_case "anchor fires" `Quick test_anchor_fires;
       Alcotest.test_case "vocab rank injectivity fires" `Quick test_vocab_rank_injectivity_fires;
-      Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires ]
+      Alcotest.test_case "vocab season injectivity fires" `Quick test_vocab_season_injectivity_fires;
+      Alcotest.test_case "slugs fires" `Quick test_slugs_fires;
+      Alcotest.test_case "lost fires on resolution exception" `Quick test_lost_fires_on_resolution_exception;
+      Alcotest.test_case "duplicated fires" `Quick test_duplicated_fires;
+      Alcotest.test_case "unconverged fires" `Quick test_unconverged_fires;
+      Alcotest.test_case "admission fires" `Quick test_admission_fires;
+      Alcotest.test_case "observed fires" `Quick test_observed_fires;
+      Alcotest.test_case "resolution checks clean on a well-behaved layer" `Quick
+        test_resolution_checks_clean_on_a_well_behaved_layer;
+      Alcotest.test_case "exhaustive domain sweep (1583..9999), committed not sampled" `Slow
+        test_exhaustive_domain_sweep ]
     @ List.map QCheck_alcotest.to_alcotest [ prop_invariants ] )