Repository navigation
Move catalog theorems out of the Challenges namespace; closure-lemma names for preserves - #2540
Merged
Merged
Conversation
…names for preserves Part C of #2534. Of the 114 public declarations in RealRooted.Challenges, 22 move into the modules that hold their proofs under library names and 92 catalog entries now point at the existing library results they wrapped; challenge files keep only their catalog entries. 45 preserves names become closure lemmas in the predicate's namespace. Six deprecated aliases keep names the downstream sequence proofs use. Naming baseline 171 -> 21; about 1000 lines fewer. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part C of #2534. Statements and proofs are unchanged; every caller, catalog entry and document is updated.
Challengesnamespace: of the 114 public declarations inRealRooted.Challenges, 22 move into the modules that hold their proofs under library names; for the other 92, which wrapped existing library results, the catalog entry now points at the library declaration and the wrapper is removed. Challenge files keep only their catalog entries and stay importable under their module paths.preservesnames: 45 become closure lemmas in the predicate's namespace (for examplereverseHermiteTransform_preserves_pf→IsPFPolynomial.reverseHermiteTransform,preservesInterlacingSeq0_iff→PreservesInterlacingSeq0.iff_nonneg_and_2x2). 21 names are kept: 14 predicate definitions, two counting theorems and five classifications without a fitting predicate namespace.@[deprecated (since := "2026-11-12")]aliases keep the names that the sequence-proof repository uses; theChallenges.Combinatorial.Eulerianmodule path and the Hermite–Poulain exports still work.Checks on this head:
lake build RealRooted.Production RealRooted.Tactic.Examplespassed;check_declaration_names.py(with--self-test),check_proof_status.py,check_root_imports.py,check_module_system.py,check_import_architecture.py,build_challenge_pages.py --check(149 pages),test_challenge_catalog.pypassed. The full rename table is in the commit history of this branch's lane notes and available on request.🤖 Generated with Claude Code