Updates manuscripts, the catalog and overview, and withdrawal notices and archive links. Adds Lean formalizations and supporting results, with documentation and an updated formalization manifest. Validation Verified all tracked file contents and executable modes against the intended release snapshot. This is a single-commit update. Lean builds were not run for this synchronization.