Repository navigation
refactor(List): move maximum-fold bounds out of the sparse-counter API #1647
Description
Follow-up to #1643 and the recorded lower-home tasks, part of #949.
Four general bounds for List.foldl max on natural numbers are public in Cslib.Complexity.SubexponentialSAT.SparsePolyCounter: foldl_max_le_iff, foldl_max_le, le_foldl_max_init, and le_foldl_max_of_mem. Boolean-analysis clients (BoundedIncidenceCounter, BoundedIncidenceSemantics, BoundedIncidenceStepCert, BoundedIncidenceExactness) and the CNF client BranchedSparseCNFCounter use them. Users of a basic list bound should not have to discover it under the sparse polynomial counter.
Search pinned Mathlib/CSLib and this library first. Reuse existing upstream facts where possible; otherwise put the existing four statements in one small List topic module, keeping their natural-number scope. Delete the application copies and update every repository client without deprecated aliases. Avoid adding declarations to the widely imported List Basic hub.
Completion criteria:
- Preserve the existing mathematical statements, hypotheses and every client resource/endpoint bound; no new generalization or parallel API.
- The intended List API has checked representative clients, with empty-list and element-dominates-initial behavior clear from existing checks or a small meaningful example.
- Preserve source credit, update the import aggregate if needed, assess curated abstracts, and pass all six validation gates plus applicable source checks before submission; obtain independent review of the final revision.
Scope is these four bounds and their clients only. The separate foldl_keep_fst, certificate-space, polynomial-bound and binary-length follow-ups remain with #949. Coordinator: codex-coord-20261029-1732. A dedicated worker will post its claim before implementation.
AI assistance: Codex prepared this bounded follow-up from the existing review and source/client inspection.
Activity
SamuelSchlesinger commentedon Oct 29, 2026
active — authoring worker
codex-worker-list-foldl-max-1647(/root/list_foldl_max) claims the four-bound reuse/move and client migration on branchwork/list-foldl-max-1647-codex, isolated worktree.worktrees/codex-list-foldl-max-1647. I am checking pinned core/Mathlib/CSLib fold/max APIs first; the existing Nat statements and all endpoint/resource bounds will be preserved. Coordinator iscodex-coord-20261029-1732.SamuelSchlesinger commentedon Oct 29, 2026
Review subtask arranged by coordinator
codex-coord-20261029-1732: non-author reviewer/root/review_list_foldl_maxis checking the frozen seven-file diff in a fresh context, with exact source hashes for matching the eventual commit. The worker found direct coreList.maxAPIs, so the implementation removes the four application helpers and matching private test duplicate without adding a module/API. Full validation remains in progress; ownership stays withcodex-worker-list-foldl-max-1647.SamuelSchlesinger commentedon Oct 29, 2026
codex-worker-list-foldl-max-1647: awaiting review in #1650 at6982088c66d3. The four public helpers and matching private test duplicate are removed, with all clients using Lean core's list maximum API. The PR records validation and the no-impact abstract assessment. Coordinatorcodex-coord-20261029-1732, please review the submitted revision.SamuelSchlesinger commentedon Oct 29, 2026
Source review completed — #1650 approval covers the committed revision under the delegated-review exception, with a separate non-author reviewing context. The bounded cleanup is awaiting hosted CI and coordinator integration; this issue stays open until merge. The PR owns final validation and review evidence.
SamuelSchlesinger commentedon Oct 29, 2026
Completed — #1650 landed on
mainas329e8c4ab6ef250c25e2c8aad748fafa2e99b08f, with successful merge-group validation. The four application helpers and private test duplicate are removed; all affected clients reuse Lean core's maximum API. Endpoint statements and resource bounds are preserved, with no new module or public API. Coordinatorcodex-coord-20261029-1732verified integration; #949 retains the broader placement follow-ups.