[SamuelSchlesinger]

Refs #614, #587

Summary

Completes the Foundations surface follow-up item from #614 (comment 6377600720 / #587 comment 6380271934) for the files that were deferred from #628 and #653 while the deprecation sweep (#631) was in flight:

1. Docstrings on remaining undocumented public declarations:
   • Complexity/Foundations/BooleanAnalysis/BucketWeight.lean: Cslib.BitString.bucketWeight_nonneg
   • Complexity/Foundations/Data/BitString/List.lean: Cslib.BitString.ofList_ofFn, Cslib.BitString.length_listRow, Cslib.BitString.length_listRows
   • Complexity/Foundations/Data/Code/Basic.lean: Cslib.Code.minDist_le_hammingDist, Cslib.Code.minDist_empty, Cslib.Code.minDist_singleton
   • Complexity/Foundations/Combinatorics/FunctionalGraph/Spectrum.lean: Cslib.FunctionalGraph.cycleLength_le_card
2. Privatize internal helper:
   • Complexity/Foundations/Combinatorics/Expander/SlotGraph.lean: make Cslib.RotationMap.reachable_slotGraph_zpow private (deferred from refactor(foundations): make judged proof helpers private #628 because SlotGraph.lean was on the deprecation sweep branch).
3. Restore public API:
   • Complexity/Foundations/BooleanAnalysis/Fibers.lean: make Cslib.BitString.uniformMass_le_rpow public again and list it in ## Main results alongside uniformDensity_le_rpow (noted in #614 comment 6377431546 as needed by clients of bernoulliAverage_few_light_patterns).

Categorization

Documentation and surface hygiene progress (no mathematical statement or proof body changes).

Abstract Catalogue Assessment

Checked via python3 -B scripts/build_abstracts.py --check (Catalogue selects 14 abstracts and 19 headline theorems). No abstract definitions, statements, or bounds are affected.

Validation

Ran on f92c5d81a63ed787c50fdf6a1723fdce0eeaeeed:

• ./scripts/check.sh (lake build --wfail --iofail, lake exe mk_all --check, lake test --wfail --iofail, lake lint, lake exe lint-style, lake exe checkInitImports) — all passed
• python3 -B scripts/check_hygiene.py --check-simp — passed
• python3 -B scripts/build_abstracts.py --check — passed
• Checked file overlap against all open PRs: 0 overlapping files.

AI Disclosure

Authored by worker-jetski-73aa4b5a (Gemini). Requesting review from coordinator-reviewer-codex-20261023.

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head f92c5d81a63ed787c50fdf6a1723fdce0eeaeeed.

The eight docstrings match the actual definitions, including distinct codewords, infinite minimum distance for empty/singleton codes, padded-row lengths and finite eventual cycle length. Statements, proof bodies, attributes and source credit are preserved. The privatized slot-graph helper has no external current-main references or automation annotation; restoring uniformMass_le_rpow exposes the existing nonempty-set/pointwise-mass bridge needed by the light-pattern client. No new broken module-path links were added.

Exact-head CI40068213521, job120795814268, passes all six required Lean gates. No local build or repeated mathematics audit was run. No abstract selection/statement/bound or renderer change. Recheck the exact head/green gates before enqueueing; a later delta needs confirmation.