[sorrachai]

Upgrade AlgoLib from Lean 4.30.0-rc2 to stable 4.35.0, with Mathlib and CSLib pinned to their matching v4.35.0 releases and a regenerated dependency manifest. Pin checkdecls to its existing revision, which builds and runs on the new toolchain.

Migrate the library to Lean's module system so a downstream module file can import AlgoLib. Most changed files only gain module headers, public imports, and exposed public declarations. Port the binary-tree and splay-tree APIs from Mathlib's deprecated Tree name to BinaryTree, make the cycle-constructor helpers available to exposed definitions, and repair graph proofs affected by changes to simplification, transparency, and numeric casts. No theorem statements are weakened or proof placeholders added.

Rewrite the README with new-project setup, TOML and Lean dependency declarations, cache downloads, imports, builds, revision pinning, and migration notes. Add a CI smoke test for public graph, BFS, and splay-tree APIs and update the import-style check to cover public import.

Validation on Lean 4.35.0:

• Full lake build passes (3,249 jobs).
• lake env lean tests/Import.lean passes.
• A separate project installs the published commit fee4f48dfb9df57be44042e6947b837a43d61d30 as a Git dependency, runs the README cache command, and builds successfully (3,251 jobs), reusing the downloaded third-party dependency cache.
• Both the TOML and lakefile.lean dependency forms resolve successfully; the README example and module-system graph/BFS/splay-tree examples compile in the consumer projects.
• checkdecls builds and verifies representative exported declarations.
• git diff --check passes; all 83 Lean source/test files were scanned for active proof placeholders and trust exceptions, with none found.

Migration note: downstream tree code should use BinaryTree, open BinaryTree, and BinaryTree.* instead of Tree, open Tree, and Tree.*. Import paths are unchanged. Existing style and deprecation warnings remain.

GitHub Actions run #105 passed: full project build, public-import/declaration-checker smoke test, and import-style check.