TankTechnology · TankTechnology · Aug 14, 2026 · Aug 12, 2026 · Aug 12, 2026 · Aug 12, 2026
diff --git a/CLRSLean/FourthEdition/Chapter_15.lean b/CLRSLean/FourthEdition/Chapter_15.lean
@@ -26,8 +26,10 @@ these sources during the compatibility period.
 
 ## Coverage boundary
 
-Section 15.4 (offline caching) is a native fourth-edition section (the
-farthest-in-future eviction policy; the optimality theorem remains a gap),
+Section 15.4 (offline caching) is a native fourth-edition section.  Its finite
+cache model, farthest-in-future policy, legal-trace exchange construction, and
+public optimality theorem `CLRS.Caching.fifo_optimal` complete CLRS Theorem
+15.5 for every nonempty initial cache and finite request sequence.  It is
 imported through
 [Section 15.4](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/).
 The section is split into the sub-modules:
@@ -36,6 +38,10 @@ The section is split into the sub-modules:
 * [Farthest-In-Future Eviction](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S2_Farthest_In_Future/)
 * [Optimality](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality/)
 
+This completion is at the mathematical cache-policy level.  Pointer/RAM
+implementations and hardware caching costs remain optional refinements outside
+the advertised theorem boundary.
+
 The third-edition Sections 16.4 (matroids) and 16.5 (task scheduling) are
 retained as supplementary online material (reachable through
 {lit}`CLRSLean.OnlineMaterial`).

diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching.lean
@@ -9,7 +9,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.S3_Optimal
 This section formalizes the offline caching problem of CLRS §15.4 and the
 farthest-in-future (Belady) eviction policy: the cache model with policies,
 hits and misses, the next-use function, the farthest-in-future selection, and
-basic sanity lemmas for the policy.
+the finite-trace exchange proof that the policy is optimal.
 
 Main results:
 
@@ -19,13 +19,17 @@ Main results:
 - `farthestInFuture cache σ i`: the resident page whose next use is farthest
 - `fifoPolicy σ`: the farthest-in-future eviction policy
 - `fifo_step_of_mem` / `fifo_step_fault`: the policy's cache transitions
+- `LegalTrace`: a policy-independent certificate for a legal cache execution
+- `fifo_optimal`: for every nonempty initial cache and finite request sequence,
+  the farthest-in-future policy incurs no more misses than any policy (CLRS
+  Theorem 15.5)
 
-Current gaps:
+Completion boundary:
 
-- The optimality theorem (`fifo_optimal`: no eviction policy has fewer
-  misses than the farthest-in-future policy, CLRS Theorem 15.5) remains to
-  be formalized; the classical exchange argument over request suffixes is
-  deferred.
+- The mathematical offline-caching optimality theorem is complete.  The result
+  is stated for finite request lists and a nonempty finite initial cache.
+  Pointer-level cache mutation, RAM costs, and hardware caching behavior are
+  separate implementation refinements and are not claimed here.
 
 Notation conventions used in this section:
 
@@ -41,4 +45,12 @@ The section is split into the following sub-modules:
 * [Cache Model](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S1_Cache_Model/)
 * [Farthest-In-Future Eviction](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S2_Farthest_In_Future/)
 * [Optimality](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/S3_Optimality/)
+* [Optimality proof overview](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/)
+* [Trace-coupling proof](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/)
+* [Legal cache traces](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A1_LegalTrace/)
+* [Exact one-page cache difference](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A2_OnePageDiff/)
+* [Recursive coupling core](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A3_CouplingCore/)
+* [Coupling correctness](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A4_CouplingCorrect/)
+* [One-step FIF exchange](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A5_Exchange/)
+* [Finite exchange iteration](CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Optimality/Trace/A6_Iteration/)
 -/
diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B3_AfterJ_Window.lean
@@ -16,7 +16,8 @@ Main results:
 - `repairSchedule_after_J_window`: the `(J, J']` window relation, by
   induction from `repairSchedule_after_J`
 
-This file is part of the `fifo_optimal` iteration (see `Dev/DESIGN.md`); it
+This file is part of the archived `fifo_optimal` iteration (see
+`Dev/Legacy/StateMachine/DESIGN.md`); it
 will be merged into `S3_Optimality.lean` once the proof is complete.
 -/
 

diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B4_Repair_Swap_Count.lean
@@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B3_Aft
 # Dev B4: the resident (B2) repair counting lemma
 
 Development file for the resident-case repair step of the `fifo_optimal`
-iteration (see `Dev/DESIGN.md`): when `q = e t` is resident, replacing the
+iteration (see `Dev/Legacy/StateMachine/DESIGN.md`): when `q = e t` is resident, replacing the
 eviction at the first disagreement by the policy's choice (`q'`, evicted
 again at its first request) costs at most one extra miss and extends
 agreement by one position — the B2 analogue of `repair_step`.

diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B5_Iteration.lean
@@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B4_Rep
 # Dev B5: the iteration to `fifo_optimal`
 
 Development file for the final assembly of the optimality proof (see
-`Dev/DESIGN.md`): starting from an arbitrary reduced schedule, repeatedly
+`Dev/Legacy/StateMachine/DESIGN.md`): starting from an arbitrary reduced schedule, repeatedly
 repair or exchange at the first disagreement with the FIF schedule, tracking
 the reducedness bound and the accumulated slack, until the schedule agrees
 with the policy everywhere; the miss count never increases overall.

diff --git a/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean b/CLRSLean/FourthEdition/Chapter_15/Section_15_4_Offline_Caching/Dev/B6_Strong_Repair.lean
@@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B5_Ite
 # Dev B6: the strong B2 repair (no slack needed)
 
 Development file for the resident (B2) repair step of the `fifo_optimal`
-iteration (see `Dev/DESIGN.md`): when `q = e t` is resident at a case-B
+iteration (see `Dev/Legacy/StateMachine/DESIGN.md`): when `q = e t` is resident at a case-B
 position, the repair `r = repairSchedule e t q'' (t+1+j'')` costs **no
 slack** — the good event at `J = t+1+j` (the repair hits where `e` faults)
 offsets the bad event at `J'' = t+1+j''`.  This is the "strong version" of

diff --git a/...Edition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md b/...Edition/Chapter_15/Section_15_4_Offline_Caching/Dev/Legacy/FAILED_APPROACHES.md
@@ -0,0 +1,152 @@
+# Failed approaches to the Chapter 15.4 optimality proof
+
+This file is the negative-results ledger for the abandoned schedule-state-machine
+proof of farthest-in-future optimality.  The archived sources are under
+`StateMachine/`; the accepted public proof instead uses legal cache traces and
+a local one-page coupling under `Optimality/Trace/`.
+
+The search counts below refute the stated invariant designs.  They are not
+claims that every enumerated state is reachable.  Explicit theorem interfaces,
+concrete counterexamples, and Lean proofs remain the authoritative evidence.
+
+## 1. Conditional final wrapper (`hB1` / `hB2` / `hAone`)
+
+- **Attempted invariant.**  `IterateState` tracked agreement, reducedness,
+  natural-number slack, historical page pairs, and repair windows.  The B7
+  iteration theorem delegated its remaining transitions to three supply
+  hypotheses `hB1`, `hB2`, and `hAone`.
+- **Failure evidence.**  The private theorem originally named `fifo_optimal`
+  (renamed `fifo_optimal_conditional_legacy` during archival) in
+  `StateMachine/B7_Iteration.lean` accepts all three supplies as arguments.
+  Kernel checking therefore establishes only a conditional implication, not
+  CLRS Theorem 15.5.  B8--B14 refine pieces of the supplies but never eliminate
+  the conditional public boundary.
+- **Reusable results.**  The schedule/cache algebra in S3, first-disagreement
+  lemmas, exchange/repair transition calculations, exact miss accounting, and
+  next-use lemmas remain useful mathematical facts.  They informed the trace
+  proof's statement shaping and local transition split.
+- **Recurrence-prevention rule.**  Completion requires an interface test that
+  instantiates `CLRS.Caching.fifo_optimal` at the approved unconditional type.
+  A theorem with any state-machine supply hypothesis cannot pass G4.
+
+## 2. Full-history `hQ`
+
+- **Attempted invariant.**  Store every historical repair pair in `Q` and
+  require every live pair's first future request (its nop position) to remain
+  strictly after the current disagreement.  The reverse-difference chain was
+  then bounded by `Q.image`.
+- **Failure evidence.**  Once a pair's nop has passed, the strict bound is
+  arithmetically impossible.  `search_hq.py` found 10,236 B1 and 688 B2 steps
+  with an old nop at or before the step, 212 B1 and 312 B2 boundary cases with
+  the nop exactly at `t₂ + 1`, and **988 B2 steps entered from an already
+  broken-`hQ` state**.  Pruning expired pairs also loses pages needed by the
+  reverse-difference chain.
+- **Reusable results.**  `b2_ehit_ne_per_page`, `last_pair_page_stays`,
+  `creditedPage`, and `HQPerPageHyp` in `StateMachine/B14_PerPageHQ.lean`
+  isolate valid consulted-pair and page-stays facts.  The reverse-difference
+  lemmas remain valid with their explicit premises.
+- **Recurrence-prevention rule.**  Never quantify a future-position bound over
+  unpruned full history without proving preservation across the boundary where
+  each stored position expires.  Test the extension step, not only consumers
+  of the invariant.
+
+## 3. Plain natural-number slack
+
+- **Attempted invariant.**  Maintain
+  `schedMisses d + slack ≤ initialMisses`, credit an exchange by one when its
+  bad event does not occur, and pay each B1 repair from the same scalar slack;
+  the key supply was `bad ≤ slack`.
+- **Failure evidence.**  Exact enumeration in `search_slack.py` found
+  **492 negative-slack executions**.  A minimal recorded counterexample is
+  `σ = [1,1,3,2,4,1,2,4]`, `C₀ = {1,2}`, with the largest-resident source:
+  an A step at 2 produces no credit, a free B2 step occurs at 4, then a real
+  B1 bad at 5 requires one unit while slack is zero.  Of 3,836 B1 bads, 1,040
+  are outside the directly covered `q₀'` case and 492 of those have zero
+  slack.
+- **Reusable results.**  `b1_exchange_no_bad_q0` and
+  `b1_bad_le_slack_q0` correctly cover the `d t₂ = q₀'` subcase.
+  `repair_step_swap_exact_net` and the exact B2 good/bad accounting are also
+  sound local results.
+- **Recurrence-prevention rule.**  A global natural-number potential must be
+  proved nonnegative at every consumer.  Aggregate miss inequalities and a
+  handful of locally credited cases do not establish a supply theorem.
+
+## 4. Per-page credit and candidate-C credit
+
+- **Attempted invariant.**  Replace scalar slack by pending-good balances per
+  page, drawing a B1 bad first from the repaired page's balance; a candidate-C
+  variant sends alive-alive B2 net savings to a global pool.
+- **Failure evidence.**  The per-page design reduces the 492 failures only to
+  336; candidate-C reduces them to **164**, not zero.  All 164 residual cases
+  contain two consecutive B1 bads in one window.  The second required page has
+  no pending good under any identified credit, so the proposed balance can go
+  negative and no closed global invariant results.
+- **Reusable results.**  The arithmetic lemmas
+  `b1_bad_le_slack_credit`, `b1_draw_credit`, `b1_draw_slack`, and
+  `b2_good_accrues` in `StateMachine/B13_PerPageCredit.lean` are correct under
+  their explicit supply premises.  They document how a future proof could
+  consume a genuinely established page credit.
+- **Recurrence-prevention rule.**  A refined credit system is not accepted
+  until exhaustive transition preservation closes every producer/consumer
+  case and the initial/final potentials are connected to misses.  Reducing a
+  counterexample count is diagnostic progress, not a proof.
+
+## 5. Skipping the case-one branch-1 position with `hnb`
+
+- **Attempted invariant.**  After a case-one exchange, raise the reducedness
+  boundary `hnb'` past the unique branch-1 no-op position, expecting the next
+  disagreement to occur after that boundary and return to case A.
+- **Failure evidence.**  `search_caseone.py` found 7,384 branch-1 spots and
+  zero multiple spots, but in every applicable trace the next disagreement
+  lands **exactly at the branch-1 spot**, hence below `hnb' = s₁ + 1`.
+  Example: `σ = [1,1,3,4,1]`, `C₀ = {1,2}`, exchange at 2, spot and next
+  disagreement at 3.  Raising `hnb` relabels the required transition as case
+  B; it does not remove it.  Unbounded junk positions also forced a vacuous
+  `σ.length + 2` boundary rather than a finite reduced tail.
+- **Reusable results.**  `case_one_D_minus_E_subset_q'`,
+  `case_one_exchange_fault_imp_d_fault`, `case_one_branch1_once`, and the
+  no-window B1 construction in B10--B12 are kernel-checked and precisely
+  describe this exceptional transition.
+- **Recurrence-prevention rule.**  A boundary shift is valid only after proving
+  the next disagreement is on the permitted side.  Always test equality at
+  the proposed boundary; do not infer progress from at-most-once alone.
+
+## 6. Build-based false completion
+
+- **Attempted criterion.**  Treat absence of `sorry`, kernel checking of every
+  local file, or a successful repository build as evidence that §15.4 is
+  complete.
+- **Failure evidence.**  The legacy tree compiled while the only final wrapper
+  was private and conditional on `hB1`, `hB2`, and `hAone`; the public section
+  did not export an unconditional `fifo_optimal`.  A build checks declarations
+  that exist, not the intended theorem that is missing.
+- **Reusable results.**  Kernel checking and unfinished-marker scans remain
+  necessary lower-level gates.  They become meaningful when combined with a
+  public interface typecheck and `#print axioms`.
+- **Recurrence-prevention rule.**  Completion is conjunctive: exact public
+  theorem type, public import reachability, acceptable axiom report, focused
+  interface instantiation, and repository checks must all pass freshly.
+
+## 7. Third-/fourth-edition migration ledger collision
+
+- **Attempted criterion.**  Reuse the existing `Chapter 15` progress row for
+  the newly migrated §15.4 work without distinguishing editions or source
+  paths.
+- **Failure evidence.**  In CLRS third edition, Chapter 15 is Dynamic
+  Programming; in the fourth edition, Chapter 15 is Greedy Algorithms and
+  contains offline caching.  FIF progress was written into the legacy Dynamic
+  Programming row, making a status claim that referred to the wrong chapter.
+- **Reusable results.**  The compatibility map and explicit fourth-edition
+  module hierarchy provide stable identities during migration.
+- **Recurrence-prevention rule.**  Every progress entry must name the edition,
+  chapter title, and canonical source path.  Never join migration ledgers by
+  chapter number alone.
+
+## Non-mathematical implementation incident
+
+Deriving `Repr` for a coupling state containing `Finset` triggered a Lean
+compiler panic on the project's release-candidate toolchain.  The instance was
+unused, so removing the derivation restored compilation without changing any
+definition or theorem.  This was a toolchain/diagnostic-surface issue, not a
+failed mathematical route; avoid deriving runtime representations for proof
+states unless a test actually needs them.
diff --git a/...ffline_Caching/Dev/B10_CaseOne_Hdred.lean → ...egacy/StateMachine/B10_CaseOne_Hdred.lean b/...ffline_Caching/Dev/B10_CaseOne_Hdred.lean → ...egacy/StateMachine/B10_CaseOne_Hdred.lean
@@ -1,4 +1,4 @@
-import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B9_Assembly
+import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B9_Assembly
 
 /-
 # Dev B10: case-one hdred supply

diff --git a/...4_Offline_Caching/Dev/B11_CaseOne_B1.lean → ...v/Legacy/StateMachine/B11_CaseOne_B1.lean b/...4_Offline_Caching/Dev/B11_CaseOne_B1.lean → ...v/Legacy/StateMachine/B11_CaseOne_B1.lean
@@ -1,4 +1,4 @@
-import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B9_Assembly
+import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B9_Assembly
 
 /-
 # Dev B11: the case-one no-window B1 step

diff --git a/...e_Caching/Dev/B12_CaseOne_NoWindowB1.lean → .../StateMachine/B12_CaseOne_NoWindowB1.lean b/...e_Caching/Dev/B12_CaseOne_NoWindowB1.lean → .../StateMachine/B12_CaseOne_NoWindowB1.lean
@@ -1,4 +1,4 @@
-import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B11_CaseOne_B1
+import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B11_CaseOne_B1
 
 /-
 # Dev B12: the no-window B1 step (case-one assembly)

diff --git a/...ffline_Caching/Dev/B13_PerPageCredit.lean → ...egacy/StateMachine/B13_PerPageCredit.lean b/...ffline_Caching/Dev/B13_PerPageCredit.lean → ...egacy/StateMachine/B13_PerPageCredit.lean
@@ -1,4 +1,4 @@
-import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B12_CaseOne_NoWindowB1
+import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B12_CaseOne_NoWindowB1
 
 /-
 # Dev B13: the per-page credit invariant (non-q₀' B1 slack)

diff --git a/..._4_Offline_Caching/Dev/B14_PerPageHQ.lean → ...ev/Legacy/StateMachine/B14_PerPageHQ.lean b/..._4_Offline_Caching/Dev/B14_PerPageHQ.lean → ...ev/Legacy/StateMachine/B14_PerPageHQ.lean
@@ -1,4 +1,4 @@
-import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B13_PerPageCredit
+import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.Legacy.StateMachine.B13_PerPageCredit
 
 /-
 # Dev B14: the per-page credit invariant — hQ replacement

diff --git a/...5_4_Offline_Caching/Dev/B7_Iteration.lean → ...Dev/Legacy/StateMachine/B7_Iteration.lean b/...5_4_Offline_Caching/Dev/B7_Iteration.lean → ...Dev/Legacy/StateMachine/B7_Iteration.lean
@@ -4,7 +4,7 @@ import CLRSLean.FourthEdition.Chapter_15.Section_15_4_Offline_Caching.Dev.B6_Str
 # Dev B7: the iteration assembly (repair diff invariants)
 
 Development file for the iteration assembly of the `fifo_optimal` proof (see
-`Dev/DESIGN.md`): the reverse-diff invariants of a B2 repair.  At a B2
+`Dev/Legacy/StateMachine/DESIGN.md`): the reverse-diff invariants of a B2 repair.  At a B2
 position `t` (inside the window of the last case-A exchange), with
 `q = e t` resident and `q'' = fifoSchedule σ C₀ t` both alive (`j < j''`),
 the repair `r = repairSchedule e t q'' (t + 1 + j'')` evicts `q''` at `t`
@@ -73,7 +73,7 @@ Main results:
   `Q' = insert (t₂, q'') Q`, `P'`, `r` from the old state's invariants
   plus the step's facts (`r t₂ = q''`, `r nop = q''`, `r s = d s` off
   `{t₂, nop}`, caches agree up to `t₂`, `σ[t₂]` fault, `q''` resident);
-  hQ's extension is the open design question (see `Dev/DESIGN.md`)
+  hQ's extension is the open design question (see `Dev/Legacy/StateMachine/DESIGN.md`)
 - `iterate_main_case_b2_alive`: the case-B2 step (alive-alive) — the
   repair at a resident disagreement: agreement to `t₂ + 1`, misses not
   increased, chain extended by `q''`, `hd_eq` extended to
@@ -100,7 +100,7 @@ Main results:
   is reduced from `t + 1` on except the branch-1 positions (`d s = q'`
   — the exchange evicts `q'` as a no-op, not resident; at most one such
   fault); the q-dead sub-case's final agreement is attainable (the
-  DESIGN's "unattainable" claim is stale — see `Dev/DESIGN.md`)
+  DESIGN's "unattainable" claim is stale — see `Dev/Legacy/StateMachine/DESIGN.md`)
 - the q₀'-B1 slack supply: `exchangeSchedule_eq_q'_imp_d_eq_q'` (the
   branch-1 reverse — the exchange evicts `q₀'` at `s > t₀` iff the source
   does), `b1_exchange_no_bad_q0` (at a B1 with `d t₂ = q₀'`, `t₂ ∉ P`,
@@ -111,7 +111,7 @@ Main results:
   gives `q₀' ∉ D₀_{J'₀}` — the exchange's bad event did not occur) and
   `b1_bad_le_slack_q0` (`bad ≤ slack` for the q₀'-B1 given `1 ≤ slack`)
   — the q₀' half of the slack accounting; the non-q₀' B1s are the open
-  design question (see `Dev/DESIGN.md`)
+  design question (see `Dev/Legacy/StateMachine/DESIGN.md`)
 
 This file is part of the `fifo_optimal` iteration; it will be merged into
 `S3_Optimality.lean` once the proof is complete.
@@ -3464,8 +3464,12 @@ private lemma iterate_main (σ : List Page) (C₀ : Finset Page) (hC₀ : C₀.N
       ∃ d' slack', agreeWithFIF d' C₀ σ σ.length ∧ schedMisses d' C₀ σ + slack' ≤ M)
     (σ.length - st.t0) hmain st rfl
 
-  /-- fifo_optimal: CLRS Theorem 15.5 via iterate_main from the initial state (d0, t0=0, slack=0, hnb=0, Q=P=empty, win=none); the hB1/hB2/hAone supplies are hypotheses. -/
-  private lemma fifo_optimal (π : Policy) (C₀ : Finset Page) (σ : List Page)
+  /-- Legacy conditional candidate for CLRS Theorem 15.5 via `iterate_main` from
+  the initial state.  This is deliberately not named `fifo_optimal`: the public
+  theorem is unconditional, while this archived route still assumes the
+  `hB1`/`hB2`/`hAone` supplies. -/
+  private lemma fifo_optimal_conditional_legacy
+      (π : Policy) (C₀ : Finset Page) (σ : List Page)
       (hC₀ : C₀.Nonempty)
       (hB1 : ∀ (M : ℕ) (st : IterateState σ C₀ M) (t₂ : ℕ) (ht₂ : t₂ < σ.length) (ht₂hnb : t₂ < st.hnb),
         agreeWithFIF st.d C₀ σ t₂ →