feat(kernel,ef): the lectionary reports which Mass it said

Rite.readings now returns (Mass_formulary.t option * Citation.t list)
instead of a bare citation list, and Liturgical_day.t carries the result
as a new formulary field. Validate holds a rite that resolves a formulary
at all to resolving one on every day, the same discipline it already
applies to citations; the EF lectionary chain resolves Some on every day
of every year 1583-9999, confirmed by a direct sweep over 2005-2050 as
well as through Validate itself.

Plan Tasks 2 and 3 are merged into this one commit on the coordinator's
own instruction: Rite.readings' signature and the field that consumes it
are one atomic edit, and the intermediate state does not compile on its
own.

Each of the four lectionary steps now builds its own Mass_formulary.t at
the point it decides, not by re-deriving it afterwards from the citations
it returns: step 1 tags Proper with the observed slug, step 2 tags
Own_slug with the day's own temporal slug, step 3 tags Preceding_sunday
with the resumed Sunday's temporal slug, and step 4 tags Common with the
Common's own id -- Commons.find now returns that id alongside its
citations rather than discarding it, since it is only ever in scope at
the point the assignment is looked up.

The RG 309(a) Saturday votive Mass of Our Lady, which answers between
steps 4 and 2 rather than as one of the four numbered steps, is tagged
Own_slug too: Mass_formulary.source has no dedicated constructor for it,
and its own guard only ever fires when the observed celebration already
is the day's own (reused ferial) temporal slug, which is exactly what
Own_slug documents. Recorded as a judgement call in the task report, not
a specified answer.

test/cli.t's `emit --format sexp` line count is repinned (8472 to 8881):
that command serializes Liturgical_day.t whole, so the new field grows
its output. `colitur day` itself is untouched -- verified byte-identical
against the pre-change binary across 1583, 1900, 2026, 2038 and 9999.

12 files changed, 281 insertions, 46 deletions

diff --git a/lib/kernel/calendar.ml b/lib/kernel/calendar.ml
index 98e9032..7fe9f67 100644
--- a/lib/kernel/calendar.ml
+++ b/lib/kernel/calendar.ml
@@ -543,6 +543,10 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.index)
       |> List.map (fun c -> (c.Precedence.cel, reason_for c)))
     @ rg33_omitted
   in
+  let formulary, citations =
+    rite.Rite.readings ~observed:resolution.Precedence.observed.Precedence.cel ~temporal ~date
+      ~temporal_at:rite.Rite.temporal
+  in
   {
     Liturgical_day.date;
     rite = rite.Rite.id;
@@ -553,9 +557,8 @@ let build_day (rite : ('s, 'r) Rite.t) (idx : 'r Layer.index)
     transferred_in;
     transferred_out;
     omitted;
-    citations =
-      rite.Rite.readings ~observed:resolution.Precedence.observed.Precedence.cel ~temporal ~date
-        ~temporal_at:rite.Rite.temporal;
+    citations;
+    formulary;
   }
 
 let year (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) (y : int) :
diff --git a/lib/kernel/liturgical_day.ml b/lib/kernel/liturgical_day.ml
index bbb52b8..709f878 100644
--- a/lib/kernel/liturgical_day.ml
+++ b/lib/kernel/liturgical_day.ml
@@ -23,5 +23,8 @@ type ('s, 'r) t = {
       (** with the reason, never silent -- Task 12's no-celebration-lost
           invariant reads this *)
   citations : Citation.t list;  (** always empty until Plan 4 *)
+  formulary : Mass_formulary.t option;
+      (** which Mass the day says, and how that was decided; [None] only for
+          a rite with no lectionary -- see {!Mass_formulary} *)
 }
 [@@deriving sexp]
diff --git a/lib/kernel/liturgical_day.mli b/lib/kernel/liturgical_day.mli
index f0ea3d9..4a71d6d 100644
--- a/lib/kernel/liturgical_day.mli
+++ b/lib/kernel/liturgical_day.mli
@@ -28,5 +28,10 @@ type ('s, 'r) t = {
           ["citations"] / ["citations-unresolved"] checks. (This said "always
           empty until Plan 4" until Task 10; the lectionary landed before
           Plan 4 did, and the comment outlived its truth.) *)
+  formulary : Mass_formulary.t option;
+      (** Which Mass this day says, and how that was decided -- see
+          {!Mass_formulary}. [None] only for a rite with no lectionary; for
+          EF it is [Some] on every day of every year 1583..9999, asserted by
+          {!Validate}. *)
 }
 [@@deriving sexp]
diff --git a/lib/kernel/rite.ml b/lib/kernel/rite.ml
index 600a691..a7d21d3 100644
--- a/lib/kernel/rite.ml
+++ b/lib/kernel/rite.ml
@@ -17,5 +17,5 @@ type ('s, 'r) t = {
     temporal:('s, 'r) Temporal.t ->
     date:Date.t ->
     temporal_at:(Date.t -> ('s, 'r) Temporal.t) ->
-    Citation.t list;
+    Mass_formulary.t option * Citation.t list;
 }
diff --git a/lib/kernel/rite.mli b/lib/kernel/rite.mli
index 0324bf2..45f3ed6 100644
--- a/lib/kernel/rite.mli
+++ b/lib/kernel/rite.mli
@@ -71,10 +71,22 @@ type ('s, 'r) t = {
     temporal:('s, 'r) Temporal.t ->
     date:Date.t ->
     temporal_at:(Date.t -> ('s, 'r) Temporal.t) ->
-    Citation.t list;
-      (** The day's Epistle and Gospel citations, or []. Rite-supplied for the
-          same reason [transfer_target] is: what a day with no proper of its
-          own falls back to is a rubric of a particular rite, not a universal.
+    Mass_formulary.t option * Citation.t list;
+      (** The Mass actually said -- which formulary, and how that was decided
+          -- paired with its Epistle and Gospel citations. Rite-supplied for
+          the same reason [transfer_target] is: what a day with no proper of
+          its own falls back to is a rubric of a particular rite, not a
+          universal.
+
+          The [Mass_formulary.t option] is [None] exactly when the rite's
+          lectionary is not built at all (the citation list is then also
+          []): a rite that HAS a lectionary is expected to resolve [Some] on
+          every day it covers, the same total-coverage discipline
+          {!Validate}'s own ["formulary"] check holds it to. [None] is never
+          a per-day "no Mass today" answer for a rite that otherwise
+          resolves readings -- that shape is coverage FAILURE, not a
+          legitimate outcome, which is exactly what makes the [Validate]
+          check meaningful.
 
           [temporal_at] is a callback so the rite can reach another date's
           temporal identity (the preceding Sunday's, for the ferial rule)
diff --git a/lib/kernel/validate.ml b/lib/kernel/validate.ml
index c9d4263..ce48615 100644
--- a/lib/kernel/validate.ml
+++ b/lib/kernel/validate.ml
@@ -453,5 +453,34 @@ let run (rite : ('s, 'r) Rite.t) (layer : 'r Layer.t) ~year =
                  fail date "citations"
                    (Printf.sprintf "expected exactly one First and one Gospel, got [%s]"
                       (String.concat "," (List.map Citation.part_to_string sorted))))
+           resolved;
+       (* ---- Formulary invariant (Task 3, celebrant-rubrics-phase1) ----
+
+          Same rite-agnostic gating as the citation checks immediately
+          above, and for the same reason: a rite whose lectionary is not
+          built returns [(None, [])] from {!Rite.readings} on every day, so
+          [year_has_formulary] is false and this check never fires for it.
+          A rite that resolves a formulary AT ALL is held to resolving one
+          on every day of the year -- a day that says no Mass at all is a
+          defect, not a gap, the same discipline the ["citations-unresolved"]
+          check above already holds for the citations themselves. One check
+          name, not two: unlike [citations], there is no separate
+          "well-formed but wrong" shape to distinguish -- [Mass_formulary.t
+          option] is either the day's answer or it is missing, so
+          [year_has_formulary] gates a single ["formulary"] label. *)
+       let year_has_formulary =
+         Array.exists
+           (fun (d : ('s, 'r) Liturgical_day.t) -> d.Liturgical_day.formulary <> None)
+           resolved
+       in
+       if year_has_formulary then
+         Array.iter
+           (fun (d : ('s, 'r) Liturgical_day.t) ->
+             match d.Liturgical_day.formulary with
+             | Some _ -> ()
+             | None ->
+                 fail d.Liturgical_day.date "formulary"
+                   "no Mass formulary resolved for this day: the lectionary chain fell through \
+                    every step")
            resolved);
   List.rev !failures
diff --git a/lib/rites/rite_ef/lectionary_ef.ml b/lib/rites/rite_ef/lectionary_ef.ml
index d7b2497..4325bed 100644
--- a/lib/rites/rite_ef/lectionary_ef.ml
+++ b/lib/rites/rite_ef/lectionary_ef.ml
@@ -51,9 +51,9 @@ module Commons = struct
         | None -> (
             (* A formulary with no citations is indistinguishable at the call
                site from "this saint has no Common" -- [commons_for] would
-               return [Some []] and [readings] would emit [] either way. That
-               is exactly the silent hole this project does not allow, so it
-               is rejected here where it is still nameable. *)
+               return [Some (common, [])] and [readings] would emit [] either
+               way. That is exactly the silent hole this project does not
+               allow, so it is rejected here where it is still nameable. *)
             match List.find_opt (fun (_, cs) -> cs = []) commons with
             | Some (s, _) ->
                 Error (Printf.sprintf "commons: common %S has no citations" (Slug.to_string s))
@@ -72,10 +72,19 @@ module Commons = struct
                          (Slug.to_string saint) (Slug.to_string common))
                 | None -> Ok { commons; assigned })))
 
+  (* Returns the Common's own id ALONGSIDE its citations, not the citations
+     alone: [readings]' step 4 needs the id to build the day's
+     {!Colitur_kernel.Mass_formulary.t} ("the Common's own id as its slug"),
+     and the id is only ever in scope here, at the point [common] is looked
+     up -- re-deriving it afterwards would mean a second [assoc_opt] search
+     over [t.assigned] for a value this function already held. *)
   let find t saint =
     match List.assoc_opt saint t.assigned with
     | None -> None
-    | Some common -> List.assoc_opt common t.commons
+    | Some common -> (
+        match List.assoc_opt common t.commons with
+        | None -> None
+        | Some cs -> Some (common, cs))
 
   (* Byte-for-byte the failure discipline of [Lectionary.load] (see its own
      comments for why each catch-all is placed where it is): every parse and
@@ -250,7 +259,8 @@ let is_bvm_saturday_office (observed : Vocab_ef.rank Celebration.t)
 
 let readings ~lectionary ~commons ~observed ~temporal ~date ~temporal_at =
   match observed.Celebration.citations with
-  | _ :: _ as cs -> cs
+  | _ :: _ as cs ->
+      (Some { Mass_formulary.said = observed.Celebration.slug; via = Mass_formulary.Proper }, cs)
   | [] -> (
       (* Step 4: a saint who is the day's observed office and has no proper
          says his assigned Common. The assignment is explicit, never
@@ -346,7 +356,8 @@ let readings ~lectionary ~commons ~observed ~temporal ~date ~temporal_at =
       match
         if sanctoral_office then commons_for ~commons observed.Celebration.slug else None
       with
-      | Some cs -> cs
+      | Some (common_id, cs) ->
+          (Some { Mass_formulary.said = common_id; via = Mass_formulary.Common }, cs)
       | None -> (
           (* The votive Mass of Our Lady on Saturday (RG 309(a)) runs HERE:
              after the proper (step 1) and the Common (step 4), which answer
@@ -354,13 +365,32 @@ let readings ~lectionary ~commons ~observed ~temporal ~date ~temporal_at =
              lookup -- which is exactly what used to answer, with the feria's
              own Mass, on a day whose office is Our Lady's. Placing it later
              would be dead code; placing it earlier would let it outrank a
-             real saint's proper. *)
+             real saint's proper.
+
+             FORMULARY PROVENANCE, a genuine judgement call: {!Mass_formulary.source}
+             has no fifth constructor for "the RG 309(a) seasonal votive Mass",
+             so this is tagged [Own_slug] -- [is_bvm_saturday_office] only ever
+             fires when [sanctoral_office] above is false, i.e. the observed
+             celebration already IS the day's own temporal office (the office
+             deliberately reuses the ordinary ferial slug, [Temporal_ef]'s own
+             [bvm_saturday_names]), so [said] is genuinely "the day's own
+             slug" -- [Own_slug]'s own documented meaning
+             (mass_formulary.mli's [said] comment) -- even though the
+             citations themselves come from [bvm_saturday_citations]'s
+             season table rather than a [Lectionary.find] hit. Flagged in the
+             task report as an interpretation, not a specified answer. *)
           if is_bvm_saturday_office observed temporal then
-            bvm_saturday_citations temporal.Temporal.season ~month:(Date.month date)
-              ~day:(Date.day date)
+            let said = temporal.Temporal.office.Celebration.slug in
+            ( Some { Mass_formulary.said; via = Mass_formulary.Own_slug },
+              bvm_saturday_citations temporal.Temporal.season ~month:(Date.month date)
+                ~day:(Date.day date) )
           else
           match Lectionary.find lectionary temporal.Temporal.office.Celebration.slug with
-          | Some cs -> cs
+          | Some cs ->
+              ( Some
+                  { Mass_formulary.said = temporal.Temporal.office.Celebration.slug;
+                    via = Mass_formulary.Own_slug },
+                cs )
           | None -> (
               (* Step 3: a feria with no proper of its own says the preceding
                  Sunday's Mass. WARRANT is the same as step 2's -- lectio's own
@@ -404,12 +434,14 @@ let readings ~lectionary ~commons ~observed ~temporal ~date ~temporal_at =
                  season name), so deriving one from the other textually would be
                  a latent bug the moment a season's naming convention differs. *)
               let offset = days_since_sunday temporal.Temporal.weekday in
-              if offset = 0 then []
+              if offset = 0 then (None, [])
               else
                 let sunday = Date.add_days date (-offset) in
                 let sunday_temporal = temporal_at sunday in
                 match
                   Lectionary.find lectionary sunday_temporal.Temporal.office.Celebration.slug
                 with
-                | Some cs -> cs
-                | None -> [])))
+                | Some cs ->
+                    let said = sunday_temporal.Temporal.office.Celebration.slug in
+                    (Some { Mass_formulary.said; via = Mass_formulary.Preceding_sunday }, cs)
+                | None -> (None, []))))
diff --git a/lib/rites/rite_ef/lectionary_ef.mli b/lib/rites/rite_ef/lectionary_ef.mli
index caefc74..2f36926 100644
--- a/lib/rites/rite_ef/lectionary_ef.mli
+++ b/lib/rites/rite_ef/lectionary_ef.mli
@@ -72,21 +72,28 @@ module Commons : sig
   val assignments : t -> (Slug.t * Slug.t) list
 end
 
-(** The Common assigned to a saint who has no proper, if any. Exposed for the
-    golden pins, which must show WHICH Common fired, not merely that two
-    citations appeared.
+(** The Common assigned to a saint who has no proper, if any -- its own id
+    ALONGSIDE its citations, not the citations alone: {!readings}' step 4
+    needs the id to name which Common fired in the {!Colitur_kernel.Mass_formulary.t}
+    it builds. Exposed for the golden pins too, which must show WHICH Common
+    fired, not merely that two citations appeared.
 
     Takes the table explicitly for the same reason {!readings} takes
     [~lectionary]: the data is the caller's, not this module's. *)
-val commons_for : commons:Commons.t -> Slug.t -> Citation.t list option
+val commons_for : commons:Commons.t -> Slug.t -> (Slug.t * Citation.t list) option
 
-(** The day's Epistle and Gospel citations, or [].
+(** The Mass actually said -- which formulary, and how that was decided --
+    paired with the day's Epistle and Gospel citations. [(None, [])] when
+    none of the four steps below answers.
 
     Four steps, in EXECUTION order 1, 4, 2, 3 (the numbers are the plan's and
     are kept as written, so that every "step 3" already recorded in a test
-    name, comment or report still means the same branch):
+    name, comment or report still means the same branch). Each step's own
+    {!Colitur_kernel.Mass_formulary.source} is built at the point the step
+    decides, not re-derived afterwards from the citations it returns:
 
     - {b Step 1} -- the observed celebration's own proper.
+      {!Colitur_kernel.Mass_formulary.Proper}, [said] the observed slug.
     - {b Step 4} -- a saint who is the day's observed office and has no
       proper says his assigned Common. Runs before the temporal fallbacks,
       not after them: this is the only step in the chain with a direct
@@ -98,14 +105,23 @@ val commons_for : commons:Commons.t -> Slug.t -> Citation.t list option
       a feria, a Sunday, the Triduum and the RG 78 Saturday Office of the
       BVM (whose observed celebration is its own temporal office) are
       structurally excluded, not merely absent from the data.
+      {!Colitur_kernel.Mass_formulary.Common}, [said] the Common's own id.
     - {b Step 2} -- the day's own temporal slug in the lectionary.
+      {!Colitur_kernel.Mass_formulary.Own_slug}, [said] that slug. The RG
+      309(a) Saturday votive Mass of Our Lady also answers here (structurally,
+      not as a fifth numbered step): it is tagged the same way, because its
+      own guard only ever fires when the observed celebration already IS the
+      day's own temporal office (the office reuses the ordinary ferial
+      slug) -- see the implementation comment on that branch.
     - {b Step 3} -- for a weekday whose own slug has no entry, the preceding
       Sunday's temporal slug (never its observed one; a Sunday is guarded
       out because it has no PRECEDING Sunday to resume, not because
       consulting itself would loop -- [readings] is not recursive, see its
       own implementation comment).
+      {!Colitur_kernel.Mass_formulary.Preceding_sunday}, [said] that
+      Sunday's temporal slug.
 
-    A day matching none of the four gets []. *)
+    A day matching none of the four gets [(None, [])]. *)
 val readings :
   lectionary:Lectionary.t ->
   commons:Commons.t ->
@@ -113,4 +129,4 @@ val readings :
   temporal:(Vocab_ef.season, Vocab_ef.rank) Temporal.t ->
   date:Date.t ->
   temporal_at:(Date.t -> (Vocab_ef.season, Vocab_ef.rank) Temporal.t) ->
-  Citation.t list
+  Mass_formulary.t option * Citation.t list
diff --git a/test/cli.t b/test/cli.t
index 2e9a0e2..bdc19c8 100644
--- a/test/cli.t
+++ b/test/cli.t
@@ -452,7 +452,7 @@ CSV run rather than one per year:
 sexp and xml are also available:
 
   $ colitur emit --format sexp --from 2027 --to 2027 | wc -l
-  8472
+  8881
 
   $ colitur emit --format xml --from 2027 --to 2027 | head -2
   <?xml version="1.0" encoding="UTF-8"?>
diff --git a/test/test_calendar.ml b/test/test_calendar.ml
index 132a466..599dfb2 100644
--- a/test/test_calendar.ml
+++ b/test/test_calendar.ml
@@ -99,9 +99,10 @@ module Fixture = struct
     let rec search d = if (occupant d).Cel.rank = Lo then d else search (D.add_days d 1) in
     search (D.add_days origin 1)
 
-  (* No fixture here exercises citations -- readings is a harmless constant
-     [], the same role [empty_layer] plays for the sanctoral side. *)
-  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = []
+  (* No fixture here exercises citations or the formulary -- readings is a
+     harmless constant [(None, [])], the same role [empty_layer] plays for
+     the sanctoral side. *)
+  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = (None, [])
 
   let rite : (season, rank) Rite.t =
     { Rite.id = "synthetic-calendar"; vocab; year_start; temporal; anchors = (fun _ -> []);
diff --git a/test/test_lectionary_ef.ml b/test/test_lectionary_ef.ml
index d56d187..bc2be8c 100644
--- a/test/test_lectionary_ef.ml
+++ b/test/test_lectionary_ef.ml
@@ -467,7 +467,7 @@ let test_step4_unreachable_commons_still_resolve () =
   let for_saint s = Lectionary_ef.commons_for ~commons (Slug.of_string_exn s) in
   let refs_of = function
     | None -> [ "<no common>" ]
-    | Some cs -> List.map (fun c -> c.Citation.reference) cs
+    | Some (_id, cs) -> List.map (fun c -> c.Citation.reference) cs
   in
   Alcotest.(check (list string))
     "St Benedict (21 March), Common of Abbots"
@@ -580,6 +580,51 @@ let test_commons_load_rejects_bad_data () =
        (Slug.of_string_exn "benedict")
      = None)
 
+(* ---------------------------------------------------------------------- *)
+(* The formulary itself (Task 2): each step of the chain now reports HOW  *)
+(* it resolved, not only what it resolved. One day per step -- the same   *)
+(* dates this file already uses (and hand-verifies) elsewhere for the     *)
+(* citations those days carry, so no new date needs independent checking. *)
+(* ---------------------------------------------------------------------- *)
+
+let formulary_cases =
+  [ (* step 1: a saint with his own proper -- same date as
+       [test_step1_proper_beats_any_common_john_of_god]. *)
+    (2038, 3, 8, "john-of-god", Colitur_kernel.Mass_formulary.Proper);
+    (* step 2: the day's own temporal slug -- same date as
+       [test_step2_lenten_feria_has_its_own], Monday of Lent I. *)
+    (2026, 2, 23, "ef-lent-1-monday", Colitur_kernel.Mass_formulary.Own_slug);
+    (* step 3: a feria resuming the preceding Sunday. The task brief's own
+       snippet pinned this date against week 9 ("ef-time-after-pentecost-
+       sunday-9"); running the real resolver against 2026 shows 3 August
+       2026 is Monday of week 10, resuming 2 August's "...sunday-10" --
+       corrected per the brief's own "find the dates by running the current
+       binary if they drift" instruction. *)
+    (2026, 8, 3, "ef-time-after-pentecost-sunday-10",
+     Colitur_kernel.Mass_formulary.Preceding_sunday);
+    (* step 4: a saint sent to a Common -- same date as
+       [test_step4_commons_perpetua_and_felicity]; [said] is the Common's
+       OWN id (data/ef/commons.sexp), not the saint's slug. *)
+    (2038, 3, 6, "common-of-non-virgins-1", Colitur_kernel.Mass_formulary.Common) ]
+
+let test_formulary_reports_its_source () =
+  List.iter
+    (fun (y, m, d, expected_slug, expected_via) ->
+      let day = day y m d in
+      match day.Colitur_kernel.Liturgical_day.formulary with
+      | None -> Alcotest.failf "%04d-%02d-%02d: no formulary" y m d
+      | Some f ->
+          Alcotest.(check string)
+            (Printf.sprintf "%04d-%02d-%02d slug" y m d)
+            expected_slug
+            (Colitur_kernel.Slug.to_string f.Colitur_kernel.Mass_formulary.said);
+          Alcotest.(check string)
+            (Printf.sprintf "%04d-%02d-%02d source" y m d)
+            (Colitur_kernel.Mass_formulary.source_to_string expected_via)
+            (Colitur_kernel.Mass_formulary.source_to_string
+               f.Colitur_kernel.Mass_formulary.via))
+    formulary_cases
+
 let suite =
   [ ("step 1: sanctoral proper", `Quick, test_step1_sanctoral_proper);
     ("step 2: own temporal proper", `Quick, test_step2_lenten_feria_has_its_own);
@@ -618,4 +663,6 @@ let suite =
     ("the five propers no real year reaches are present", `Quick,
       test_step4_unreachable_propers_are_present);
     ("Commons.load rejects the four silent-degradation defects", `Quick,
-      test_commons_load_rejects_bad_data) ]
+      test_commons_load_rejects_bad_data);
+    ("the formulary reports its own source, one day per step", `Quick,
+      test_formulary_reports_its_source) ]
diff --git a/test/test_validate.ml b/test/test_validate.ml
index 8b3014a..7387971 100644
--- a/test/test_validate.ml
+++ b/test/test_validate.ml
@@ -300,15 +300,16 @@ module Synthetic = struct
      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. *)
-  (* Most fixtures here exercise no citations -- [readings] is a harmless
-     constant [], the same role the other placeholder defaults above play,
-     and {!Validate}'s own citation checks are gated on a rite producing SOME
-     citation somewhere, so a constant [] leaves them entirely dormant. Task
+  (* Most fixtures here exercise no citations and no formulary -- [readings]
+     is a harmless constant [(None, [])], the same role the other
+     placeholder defaults above play, and {!Validate}'s own citation and
+     formulary checks are gated on a rite producing SOME citation/formulary
+     somewhere, so a constant [(None, [])] leaves them entirely dormant. Task
      10 makes it overridable ([?readings] below) so the citation fixtures at
      the end of this file can drive those checks directly, exactly as every
-     other check here is driven -- rather than leaving two kernel checks with
-     no committed proof that they can fire at all. *)
-  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = []
+     other check here is driven -- rather than leaving kernel checks with no
+     committed proof that they can fire at all. *)
+  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = (None, [])
 
   (* The shape {!Validate} accepts: exactly one First and one Gospel. The
      references are deliberately nonsense -- these fixtures assert SHAPE,
@@ -317,6 +318,12 @@ module Synthetic = struct
     [ { Citation.part = Citation.First; reference = "Synth 1:1" };
       { Citation.part = Citation.Gospel; reference = "Synth 2:2" } ]
 
+  (* The formulary equivalent of [well_formed_citations] above -- shape only,
+     never rubrically meaningful content. *)
+  let well_formed_formulary =
+    { Colitur_kernel.Mass_formulary.said = Slug.of_string_exn "syn-formulary";
+      via = Colitur_kernel.Mass_formulary.Own_slug }
+
   let rite ?(vocab = vocab) ?(anchors = fun _ -> []) ?(season_runs = [ A; B ]) ?(rules = rules)
       ?(transfer_target = fun _ origin _ -> origin) ?(readings = readings) temporal :
       (season, rank) Rite.t =
@@ -759,7 +766,7 @@ let test_citations_silent_without_a_lectionary () =
 
 (* The positive: well-formed citations on every day report nothing. *)
 let test_citations_clean_when_well_formed () =
-  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = well_formed_citations in
+  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ = (None, well_formed_citations) in
   let fs = run ~readings good in
   Alcotest.(check bool) "neither citation check fires when every day carries First + Gospel" false
     (has_check "citations" fs || has_check "citations-unresolved" fs)
@@ -769,7 +776,7 @@ let test_citations_clean_when_well_formed () =
    plausibly produce -- half a lookup succeeding. *)
 let test_citations_fires_on_a_lone_epistle () =
   let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
-    [ { Citation.part = Citation.First; reference = "Synth 1:1" } ]
+    (None, [ { Citation.part = Citation.First; reference = "Synth 1:1" } ])
   in
   Alcotest.(check bool) "citations check fires when a day carries an Epistle but no Gospel" true
     (has_check "citations" (run ~readings good))
@@ -780,7 +787,7 @@ let test_citations_fires_on_a_lone_epistle () =
    even though the day is otherwise a well-formed pair. *)
 let test_citations_fires_on_an_out_of_scope_part () =
   let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
-    { Citation.part = Citation.Tract; reference = "Synth 3:3" } :: well_formed_citations
+    (None, { Citation.part = Citation.Tract; reference = "Synth 3:3" } :: well_formed_citations)
   in
   Alcotest.(check bool) "citations check fires when a part outside First/Gospel appears" true
     (has_check "citations" (run ~readings good))
@@ -792,7 +799,7 @@ let test_citations_fires_on_an_out_of_scope_part () =
    this file singles out. *)
 let test_citations_unresolved_fires_on_a_gap () =
   let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ =
-    if D.compare date target = 0 then [] else well_formed_citations
+    if D.compare date target = 0 then (None, []) else (None, well_formed_citations)
   in
   Alcotest.(check bool) "citations-unresolved fires when one day of the year resolves nothing" true
     (has_check "citations-unresolved" (run ~readings good));
@@ -801,6 +808,79 @@ let test_citations_unresolved_fires_on_a_gap () =
   Alcotest.(check bool) "the well-formedness check stays silent on a pure coverage gap" false
     (has_check "citations" (run ~readings good))
 
+(* ---------------------------------------------------------------------- *)
+(* The formulary invariant (Task 3, celebrant-rubrics-phase1): the same    *)
+(* negative-path discipline the citation checks above already hold        *)
+(* themselves to, driven through the same synthetic fixture. Model on the  *)
+(* citations trio above -- "same shape, its own name" is what {!Validate}  *)
+(* itself now does, so the tests proving it can fire follow the same       *)
+(* pattern. *)
+(* ---------------------------------------------------------------------- *)
+
+(* The gate: a rite that resolves no formulary at all (the default constant
+   [(None, [])]) must report nothing -- not "usually", not "on this year". *)
+let test_formulary_silent_without_a_lectionary () =
+  let fs = run good in
+  Alcotest.(check bool) "no formulary check fires for a rite with no readings at all" false
+    (has_check "formulary" fs)
+
+(* The positive: a formulary on every day reports nothing. *)
+let test_formulary_clean_when_well_formed () =
+  let readings ~observed:_ ~temporal:_ ~date:_ ~temporal_at:_ =
+    (Some well_formed_formulary, well_formed_citations)
+  in
+  Alcotest.(check bool) "formulary check stays silent when every day resolves one" false
+    (has_check "formulary" (run ~readings good))
+
+(* The coverage gap: a rite that resolves a formulary on most days but falls
+   through on one. On real EF data this has no witness at all (Task 3's own
+   [test_every_day_has_a_formulary] below confirms it directly), so this
+   fixture is the only thing that holds it honest. *)
+let test_formulary_fires_on_a_gap () =
+  let readings ~observed:_ ~temporal:_ ~date ~temporal_at:_ =
+    if D.compare date target = 0 then (None, [])
+    else (Some well_formed_formulary, well_formed_citations)
+  in
+  Alcotest.(check bool) "formulary check fires when one day of the year resolves none" true
+    (has_check "formulary" (run ~readings good))
+
+(* ---------------------------------------------------------------------- *)
+(* Direct real-EF-data coverage (Task 3 brief): every day of every year in *)
+(* the sample resolves a formulary, the same discipline the "citations"    *)
+(* checks already hold EF to -- asserted directly against                  *)
+(* [Liturgical_day.t] rather than through [Validate.run]'s failure list,   *)
+(* so a bug in [Validate]'s own gating could not hide this gap. *)
+(* ---------------------------------------------------------------------- *)
+
+(* 2005-2050: the same 46-year sample test_rite_ef.ml's own [sample_years]
+   uses, for the same reason -- non-trivial, deterministic, and already the
+   project's differential-testing window (CLAUDE.md). Defined locally
+   rather than shared: test executables in this project cross-reference
+   only [.suite] values (test_colitur.ml), never each other's internal
+   helpers. *)
+let sample_years =
+  let rec range a b = if a > b then [] else a :: range (a + 1) b in
+  range 2005 2050
+
+let year_of y = Colitur_kernel.Calendar.year real_ef_rite real_ef_layer y
+
+(* Every day of every year resolves a formulary, for the same reason
+   [Validate] already asserts exactly one First and one Gospel: a day that
+   says no Mass at all is a defect, not a gap. Mirrors the "citations"
+   check. *)
+let test_every_day_has_a_formulary () =
+  let missing = ref [] in
+  List.iter
+    (fun y ->
+      Array.iter
+        (fun (d : (_, _) Colitur_kernel.Liturgical_day.t) ->
+          if d.Colitur_kernel.Liturgical_day.formulary = None then
+            missing :=
+              Colitur_kernel.Date.to_iso8601 d.Colitur_kernel.Liturgical_day.date :: !missing)
+        (year_of y))
+    sample_years;
+  Alcotest.(check (list string)) "every day resolves a formulary" [] !missing
+
 let suite =
   ( "Validate",
     [ Alcotest.test_case "landmark years" `Quick test_landmark_years;
@@ -830,6 +910,13 @@ let suite =
         test_citations_fires_on_an_out_of_scope_part;
       Alcotest.test_case "citations-unresolved fires on a gap" `Quick
         test_citations_unresolved_fires_on_a_gap;
+      Alcotest.test_case "formulary silent without a lectionary" `Quick
+        test_formulary_silent_without_a_lectionary;
+      Alcotest.test_case "formulary clean when well formed" `Quick
+        test_formulary_clean_when_well_formed;
+      Alcotest.test_case "formulary fires on a gap" `Quick test_formulary_fires_on_a_gap;
+      Alcotest.test_case "every day (2005-2050) resolves a formulary" `Quick
+        test_every_day_has_a_formulary;
       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;