perf(list): split Basic into narrow topic modules and migrate consumers

Milestone for #569, plan item 2. Split Complexity/Foundations/Data/List/Basic.lean into narrow list-topic modules, keep Basic as a thin compatibility re-export, and migrate actual consumers to the required narrow imports. Preserve all declaration names, statement shapes, attributes and source credit; avoid import cycles. This is dependency-structure infrastructure, not new mathematics.

Initial topic inventory: fold invariants/selection, defaulted lookup, list updates/register-file bounds, range tabulation, predicate counts, flat-map lengths, adjacent pairs, membership scans and unary headers. Confirm the final grouping against actual consumers and existing foundational modules before implementation.

Done when every original declaration remains accessible from the old import, narrow modules are used by real consumers, identical-scope before/after library transitive-importer counts show reduced fan-out for representative topic additions, all six repository gates pass, and independent review covers the final revision. Assess abstract/bridge impact and preserve any checked declaration locations or compatibility routes required by consumers. No wall-time or cache-hit-rate claim follows from importer counts.

Ownership: worker-codex-01a16ab8-list-basic, delegated by coordinator-codex-01a16ab8. Branch perf/list-basic-topics-569; new isolated worktree /home/samuel/Code/complexitylib-codex/list-basic, starting from landed main ba134c18. Claude owns #569 item 1 (guidance); no competing guidance edits or follow-on PMF/BitString splits are included.

blocked on integration order (worker-codex-01a16ab8-list-basic): coordinator Claude requested that source edits wait until #559, #560 and #568 land, to avoid import churn. No source edits have been made. Continuing read-only topic/consumer and import-graph analysis; implementation will resume after the gate clears.

Read-only grouping analysis is complete. The coordinator approved four coherent modules instead of the initial nine: Fold (2 declarations), Lookup (8: defaulted access, updates, bounds and range tabulation), Counting (3: scans/counts and flat-map lengths), and Append (3: adjacency boundaries and unary delimiters). Every actual consumer needs at most one topic import, so this avoids adding import lines or five extra navigation files. Basic remains a thin compatibility re-export, with every declaration name and proof preserved.

Implementation remains gated on #559/#560/#568 landing. The final PR will include a reproducible source-import graph script with exact base/head references and a fixed original-file universe. The fold group is a known limit: the current read-only model has 530 downstream library modules versus the old hub's 563; larger reductions apply to the other groups, not to every possible edit. These are planning predictions, not validated post-split measurements or build-time claims.

The four-module split is supported by recent interface churn, not just hypothetical fan-out. I inspected git log -p at exact base ba134c185f6b76f68bd31c3a6b89abe8afd0f3c6 over the four days ending at #569 creation: 2026-10-19 22:03:28 UTC through 2026-10-23 22:03:28 UTC. There are 14 non-merge commits touching List/Basic, plus three merge resolutions.

Commit	Proposed destination	Change within `List/Basic`
`ca7a33d1`	Lookup	Add `map_range_eq_ofFn`; proof-only OfFn import accompanies it
`4c1fcab8`	Append	Add `zip_tail_append_cons`
`946f5a4b`	Lookup	Add `getD_map_range`
`0e84efe6`	Counting	Move `countP_and_not_add_countP_and` into the module
`98c81881`	Lookup	Add shared `getD_idxOf`
`b198618a`	Fold	Extract `foldl_take_invariant`
`c9072f50`	Append	Add both unary-delimiter injectivity lemmas; preserve source credit
`dcbc89d8`	Lookup	Add shared `getD_mem_or`
`ca2f92a5`	Lookup	Rename `forall_mem_set` to `forall_mem_set_of_forall_mem`
`ad887c0f`	Lookup	Add four shared register-file lemmas
`f6d09f5d`	Counting	Move/generalize `decide_mem_eq_any` into the module
`51944df4`	Counting / existing OfFn home	Remove `countP_range_eq_card_filter` from Basic and move it to `List/OfFn`; narrow public imports
`4ac8dd31`	Counting	Add shared `length_flatMap_le`
`e078395c`	Counting / later OfFn home	Initially place `countP_range_eq_card_filter` here

Classification: Lookup 6, Counting 5, Append 2, Fold 1. Twelve commits add or relocate public theorem declarations into this module; one renames a public declaration and one removes/relocates one. None of these fourteen is merely a proof-body edit or an exposed-definition-body change. They are interface-affecting source categories, not fourteen separately measured rebuilds. countP_range_eq_card_filter was temporary here and is already in OfFn at the base; the split will not move it back.

The three merges are not counted again as independent additions: bfb7529a unions the Counting additions; efefbe75 resolves Counting's relocation against Lookup's new register lemmas; b70ae996 unions Counting's membership lemma with Lookup's register lemmas. git show --remerge-diff confirms these combine existing branch work; the latter two span groups. No non-merge edit in this window spans the proposed groups.

Only one of fourteen non-merge interface edits is Fold, so Fold's remaining 530/563 downstream reach is a real limitation but does not dominate this observed window. The spread supports four coherent modules while avoiding the original nine-file navigation cost. Current-graph reach and this history are separate evidence; neither establishes historical wall-time savings or actual cache invalidations.

Reproduce the history with:

git log ba134c185f6b76f68bd31c3a6b89abe8afd0f3c6 --no-merges \
  --since='2026-10-19T22:03:28Z' --until='2026-10-23T22:03:28Z' -p \
  -- Complexity/Foundations/Data/List/Basic.lean

No source edits have been made; the integration-order gate remains in effect.

Coordination update (coordinator-codex-01a16ab8): #559, #560 and #568 have landed, so the old integration-order hold is cleared. The four-topic plan and the 14-commit churn classification above remain the implementation basis, with List/Basic retained as a re-export. No source edits were started by that worker. Implementation is available while this pool is fully occupied with the priority plain-API migration and existing integration work; a new claimant should check current source/open-PR overlap and preserve the completed analysis rather than repeat it. This is a capacity handoff, not a claim that the split is done.

Active — worker codex-review-559, delegated by coordinator-codex-01a16ab8, takes the released implementation of #573. Branch perf/list-basic-topics-codex-573, isolated worktree .worktrees/codex-list-basic-573, starting at main 6182be25fe212e2c70114e7676132ff14a8c4c8f.

Preserve the completed four-topic plan and 14-commit churn analysis above: extract Fold/Lookup/Counting/Append, retain Basic as a thin re-export with unchanged declaration names/statements/proofs/attributes/credit, narrow actual consumers, and measure identical-scope fan-out before/after. No new analysis/history campaign or mathematical/API renaming. Creating files alone does not complete this issue.

Current overlap check: Basic and all four target paths are free; 25 direct library consumers and the Reingold test are free. Three consumers overlap #656 (Problems/Coloring.lean, Problems/USTCON.lean, TreeEval/Encoding.lean) and remain untouched pending coordinator resolution; the generated root aggregate also needs import-union coordination. The old deprecation sweep #631 is merged, and the current tidy-sweep PR changes tooling only. Independent files can proceed. Existing #553/#499/#681 review fixes take priority.

Setup checkpoint — worker codex-review-559: the shared origin/main ref advanced during worktree creation. The actual isolated baseline is 49f23adaef20a83e93ac3e9409cfaf917cf3e2ae, verified against GitHub main, not the earlier 6182be25 claim snapshot. List/Basic is byte-identical between them. The approved disjoint extraction/consumer scope is unchanged; #656’s three files remain held until it lands.

Active checkpoint — worker codex-review-559: the disjoint implementation is committed at f192de3e. Four topics and the old Basic re-export compile; disjoint actual consumers and Reingold pass, all sixteen declaration statements/proofs are unchanged, and an ordinary old-Basic-only import resolves every declaration. The scoped comparison reuses the native header parser and shared quality-report closure, with a fixture checking traversal through new modules before restricting the counted universe.

Consumer migration is not complete: #656 still owns Coloring, USTCON and TreeEval/Encoding. Actual-use inspection also found Geography Reduction (in #656) relying on Basic through GeneralizedGeography’s public re-export. Geography Membership now imports Counting directly; Reduction and the broad re-export removal remain held. Final original-universe measurements and all six gates will cover the complete delta after this overlap clears. No completion or build-time saving is claimed.

Active — worker codex-review-559: #656 has merged. Current open-PR overlap recheck leaves only the coordinator-approved generated root import union. Refreshing the owned checkpoint onto pinned main 268d63c9, then completing the held consumer imports and Geography re-export removal before final fixed-universe measurements and all six gates. Existing integration-review fixes remain first priority.

refactor(list): split Basic into topic modules and narrow free clients

refactor(list): finish consumer imports after the documentation merge

doc(list): point roadmap and upstream notes to the topic homes

Awaiting independent review — worker codex-review-559: #687 at 77b11766 implements the complete four-topic split, actual consumer migration and fixed-original-universe measurement. All six gates pass at the identical-source 4fdda30d checkpoint; the final commit changes only the two coordinated documentation references. The PR records source/measurement evidence, Fold’s remaining reach and the lack of a build-time claim. This issue remains open pending review and merge.

Completed through #687, now merged. The four narrow topic modules and actual consumer imports are in place; List/Basic remains a re-export for compatibility. The PR records the fixed-universe import-reach evidence and Fold’s remaining fan-out. Broader cache/build work remains under #569; this milestone makes no measured build-time claim.

perf(list): split list helpers and narrow consumers (cslib-community#687

Navigation Menu

Repository navigation

perf(list): split Basic into narrow topic modules and migrate consumers #573

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

perf(list): split Basic into narrow topic modules and migrate consumers #573

Description

Activity

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 23, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

SamuelSchlesinger commented on Oct 24, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions