Skip to content

Complete Chapter 15.4 FIF optimality integration - #215

Merged
TankTechnology merged 11 commits into
mainfrom
codex/ch15-trace-integration
Aug 14, 2026
Merged

Complete Chapter 15.4 FIF optimality integration#215
TankTechnology merged 11 commits into
mainfrom
codex/ch15-trace-integration

Conversation

@TankTechnology

Copy link
Copy Markdown
Owner

Summary

  • integrate the complete legal-trace coupling proof of farthest-in-future optimality
  • expose the unconditional CLRS.Caching.fifo_optimal theorem and lock its contract
  • preserve the known failed state-machine routes under Dev/Legacy
  • reconcile Chapter 15 status, proof ledgers, reader navigation, and literate-site registration

Verification

  • lake build CLRSLean.FourthEdition.Chapter_15 CLRSLean.Progress CLRSLean.Status
  • lake env lean Tests/Chapter_15_4_Interface.lean
  • python3 scripts/check_repository.py
  • unfinished-marker, stale-name, and public Legacy-import scans
  • independent review: no critical, important, or minor findings

A local full-repository Lean build was intentionally avoided because it is expensive. The manual Lean Action CI workflow will run the repository-wide build on this branch before merge.

@TankTechnology
TankTechnology merged commit 62271af into main Aug 14, 2026
1 check passed
@TankTechnology
TankTechnology deleted the codex/ch15-trace-integration branch August 14, 2026 02:44
TankTechnology added a commit that referenced this pull request Aug 14, 2026
Note that the six-phase maintenance cleanup is complete: the ledger audit
is reconciled, branch hygiene is done, and the final Pages deployment
(`Build and deploy Verso site` run #215) succeeded.

Co-authored-by: Claude <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant