kernel(validate): resolution invariants

Widen Validate.run to take the rite's sanctoral layer alongside the rite
itself (Calendar.year needs both), and add five checks over the fully
resolved liturgical year, on top of the existing temporal-only pass:

- observed: a day's observed celebration never also appears among that
  same day's own commemorations/omissions.
- lost: no sanctoral entry is silently dropped. Per slug, the number of
  times it is actually sighted (observed + commemorations + omitted,
  summed over the year) must never fall below the number of times its
  own Date_spec resolves within the year's span -- also fires if
  resolving the year raises at all, the most total form of loss.
- duplicated: the same per-slug count must never exceed the number of
  Date_spec resolutions either. Deliberately NOT "no slug appears
  twice": a fixed date can legitimately resolve twice in the ~20% of
  liturgical years whose 371-day span reaches it on both ends (30
  November/St Andrew is the worked example in validate.mli).
- unconverged: no day's omitted reason indicates Calendar's placement
  pass hit its round guard before reaching a fixed point.
- admission: the rite's own rules.admit is a fixed point on what it
  already admitted -- the rite-agnostic form of "the admission limit
  was not exceeded" available without embedding a rite's own numeric
  caps (RG 111's, for EF) into kernel code.

Each check has a dedicated negative fixture in the synthetic rite
(test_validate.ml), hand-traced against Calendar's actual resolution
mechanics before writing the assertion, and verified to fail for the
right reason against the code before this change. One pair
(unconverged/duplicated) is not fully independent: hitting the round
guard genuinely also trips duplicated, a real consequence of Calendar's
own accounting once a candidate is simultaneously sighted at its
permanent natural date and wherever the last placement round left it --
documented in guard_rules's own comment, not papered over.

test_validate.ml's ef_rite/run now use the real Rite_ef.context and the
real bootstrapped data/ef layer (Precedence_ef and the sanctoral
bootstrap did not exist when this scaffolding was first written) rather
than the earlier placeholder rules. Validate is clean across the whole
1583..9999 domain against real EF data except the one already-documented
year-9999 truncation case (test_year_9999_does_not_raise).

1 files changed, 43 insertions, 3 deletions

diff --git a/lib/kernel/validate.mli b/lib/kernel/validate.mli
index d281f9a..511c78f 100644
--- a/lib/kernel/validate.mli
+++ b/lib/kernel/validate.mli
@@ -5,8 +5,9 @@ type failure = { year : int; date : string; check : string; detail : string }
 
 val failure_to_string : failure -> string
 
-(** [run rite ~year] returns every invariant violation in the liturgical year
-    opening in civil year [year]. An empty list means the year is clean.
+(** [run rite layer ~year] returns every invariant violation in the
+    liturgical year opening in civil year [year]. An empty list means the
+    year is clean.
 
     [rite.Rite.anchors y] is the rite's own independent restatement of its
     fixed and Easter-derived named days for civil year [y], as (expected
@@ -21,8 +22,47 @@ val failure_to_string : failure -> string
     have one season appear in two separate runs (the modern form's Ordinary
     Time does), so the two are not necessarily the same list.
 
+    [layer] is resolved against [rite] via {!Calendar.year} (spec §2.4's
+    occurrence/transfer/commemoration pass), and the resulting fully-resolved
+    liturgical year is checked for five further invariants a temporal-only
+    pass cannot see (Task 12), each its own ["check"] label:
+    - ["observed"]: a day's [observed] celebration is never ALSO listed among
+      that same day's [commemorations] or [omitted] -- a day reports one
+      winner, not a winner that also lost to itself.
+    - ["lost"]: no sanctoral entry is silently dropped. Per slug, the number
+      of times it is actually sighted ([observed] + [commemorations] +
+      [omitted], summed over the whole year -- NOT [transferred_out], which
+      would double-count a successfully placed transfer against its own
+      arrival) must never fall below the number of times its own
+      {!Date_spec} resolves within the year's span (an entry with two
+      occurrences, e.g. 30 November in the nine liturgical years where the
+      371-day span reaches it twice, must be sighted twice, not once). Also
+      fires if resolving the year raises at all -- an escaping exception is
+      the most total form of silent loss, and the kernel contract forbids
+      [run] itself from propagating it.
+    - ["duplicated"]: the same per-slug count must never EXCEED the number of
+      {!Date_spec} resolutions either. Deliberately NOT "no slug appears
+      twice in the year" -- a fixed date can legitimately resolve twice, per
+      ["lost"] above -- it is "resolutions and sightings agree", the property
+      that actually distinguishes a transfer that moved from one that
+      duplicated.
+    - ["unconverged"]: no day's [omitted] carries the reason {!Calendar}'s
+      placement pass records when its round guard (calendar.ml's
+      [max_transfer_rounds]) is hit before every deferred candidate reaches a
+      fixed point.
+    - ["admission"]: the rite's own [rules.admit] is a fixed point on what it
+      already admitted -- re-offering a day's [commemorations] back to
+      [admit] (reconstructed with {!Precedence.Sanctoral} origin; the real EF
+      admit reads only rank and slug, never origin, so this reconstruction is
+      exact for it) must return exactly that same set. A cap-enforcing
+      selector that is not idempotent on its own output has, by definition,
+      admitted something its own rule would not admit if asked again -- the
+      rite-agnostic form of "the admission limit was not exceeded" available
+      without embedding a rite's specific numeric caps (RG 111's, for EF)
+      into kernel code.
+
     Total over the whole 1583..9999 domain, including [year] = 9999: the
     liturgical year opening there continues into out-of-domain civil year
     10000, so the walk is clamped to 31 December 9999 and the checks run
     against that truncated final year rather than raising. *)
-val run : ('s, 'r) Rite.t -> year:int -> failure list
+val run : ('s, 'r) Rite.t -> 'r Layer.t -> year:int -> failure list