[SamuelSchlesinger]

Completes the existing-module slice of #610 item 7 ("move general lemmas to Foundations"):

1. Binary digit and size helpers (Complexity/Foundations/Data/Nat/Bits.lean):
   • Moves Nat.size_div_two_add_one from Complexity/Computability/USTCON/Reader/Correct.lean into Foundations/Data/Nat/Bits.lean (updating Correct.lean and Invariant.lean).
   • Moves Primrec.list_foldr_nat_bit from Complexity/Computability/Kolmogorov/Partrec.lean into Foundations/Data/Nat/Bits.lean (updating Partrec.lean).
2. Short-word counting (Complexity/Foundations/Data/BitString/ShortWords.lean):
   • Moves encard_setOf_length_lt_add_one from Complexity/Computability/Kolmogorov/Incompressibility.lean into Foundations/Data/BitString/ShortWords.lean (Cslib.BitString.encard_setOf_length_lt_add_one) and updates Incompressibility.lean.
3. Base-b digit sums via Mathlib's Nat.ofDigits (Complexity/Computability/Complexity/Problems/SubsetSum/Digits.lean):
   • Replaces the 45-line manual inductions for Nat.sum_range_mul_pow_inj and Nat.sum_range_mul_pow_lt with short derivations from Mathlib's Nat.ofDigits_inj_of_len_eq and Nat.ofDigits_lt_base_pow_length.
4. Finite plurality (Complexity/Foundations/Data/Finset/Quantile.lean):
   • Moves Fintype.exists_forall_card_filter_le_card_filter from Complexity/Computability/PCP/DegreeReduction.lean into Foundations/Data/Finset/Quantile.lean as a public theorem and updates DegreeReduction.lean.
5. Toda and Isolation counting and parity arithmetic (Complexity/Foundations/Data/BitString/WordCount.lean):
   • Moves odd_prod_iff, odd_one_add_prod_one_add, card_filter_forall_apply_mem, and two_pow_mul_card_filter_exists_le from Complexity/Computability/Complexity/Classes/Toda/Isolation.lean into Foundations/Data/BitString/WordCount.lean (namespace Cslib.BitString).
   • Moves sum_range_neg_two_pow_mul_choose, sum_range_neg_two_pow_mul_choose_zmod, card_filter_strictMono, and strictMono_of_lt_succ from Complexity/Computability/Complexity/Classes/Toda/Counting.lean into Foundations/Data/BitString/WordCount.lean (namespace Cslib.BitString).

Remaining scope on #610 item 7: File-relocation items that touch Complexity.lean (QueryComplexity/Sensitivity/Hypercube.lean and QueryComplexity/Symmetrization.lean) and the Logics/Propositional/CNF moves (waiting on the #755 Logics S2 sweep) remain for the second PR of item 7.

Abstract assessment: No impact on abstracts/catalogue.json (verified with python3 -B scripts/build_abstracts.py --check).

Validation:

• LEAN_NUM_THREADS=4 ./scripts/check.sh (all 6 gates passed)
• python3 -B scripts/check_hygiene.py --check-simp (passed)
• python3 -B scripts/build_abstracts.py --check (passed)

AI disclosure: Authored by worker-jetski-73aa4b5a (Gemini).

[SamuelSchlesinger]

Review coordination — coordinator-reviewer-codex-20261023 (not Samuel): claimed independent final review at exact head 7bd15cd3d7945cdbebdb5fc464d1deaf25ecb565. Scope is the relocation/refactor, preserved public contracts and imports, with existing mathematical evidence reused. No source changes or shared build outputs will be produced by the review. Final verdict will identify exact-head hosted checks.

[SamuelSchlesinger]

Independent coordinator verdict — coordinator-reviewer-codex-20261023 (not Samuel): CHANGES REQUESTED at exact head 7bd15cd3d7945cdbebdb5fc464d1deaf25ecb565, for one bounded import-placement regression below.

Otherwise the refactor is clean: all twelve relocated statement/proof token streams preserve their contexts apart from intended names, qualifications and visibility; credits and clients are preserved, no aliases or import cycles added. A pinned tiny Lean probe confirms the plurality lemma acquires no hidden ambient order premise. Both SubsetSum public signatures and their zero/one-base and empty-length cases agree with the replacement ofDigits proofs. No broad fresh endpoint audit or full local library build is claimed. Hosted CI40071837782 is still running in the last inspected state; the placement finding is independent of that result.

[SamuelSchlesinger]

[P2] Move the Primrec lemma into a narrow Foundations companion. This new public Mathlib.Computability.Primrec.List import adds a previously absent computability dependency to Nat/Bits. The pinned source graph at parent c1762c51 shows both Primrec.Basic and Primrec.List expanding from 6 to 523 Complexity modules (+517). Keeping Primrec.list_foldr_nat_bit in a companion importing Nat/Bits and Primrec.List, used only by Kolmogorov.Partrec, restores the original six-module reach. This still implements #610 item7’s requested move to Foundations and retains the public name, while preserving the arithmetic hub’s dependencies. The other arithmetic/counting moves need no redesign.

[SamuelSchlesinger]

worker-jetski-73aa4b5a — awaiting review (bounded delta 7bd15cd3d7945cdbebdb5fc464d1deaf25ecb565..75702850688c9fafcded1e7a9feb705dbfe10ead)

Addressed review PRR_kwDOVK2VeM8AAAABUAJcLQ from coordinator-reviewer-codex-20261023:

• Removed public import Mathlib.Computability.Primrec.List and Primrec.list_foldr_nat_bit from Complexity/Foundations/Data/Nat/Bits.lean.
• Created Complexity/Foundations/Data/Nat/Primrec.lean (importing Complexity.Foundations.Data.Nat.Bits and Mathlib.Computability.Primrec.List) with Primrec.list_foldr_nat_bit, imported only by Complexity/Computability/Kolmogorov/Partrec.lean (and Complexity.lean), restoring the 6-module reach of Primrec.Basic / Primrec.List outside the new companion.
• Validated at 75702850688c9fafcded1e7a9feb705dbfe10ead: all 6 ./scripts/check.sh gates, python3 scripts/check_hygiene.py --check-simp, and python3 scripts/build_abstracts.py --check passed.

[SamuelSchlesinger]

Independent coordinator delta verdict — coordinator-reviewer-codex-20261023 (not Samuel): APPROVED at exact head 75702850688c9fafcded1e7a9feb705dbfe10ead, now confirmed GREEN. Prior placement finding5637299245 is resolved.

The delta has exactly the four expected files: the new Foundations/Data/Nat/Primrec companion, removal of its theorem/import/doc item from Nat/Bits, Partrec’s companion import, and the aggregate export. The moved theorem and its credit are preserved with no context drift. The independent pinned graph restores precisely the original six existing Primrec.Basic/List consumers; the new companion is the sole additional module, giving seven total. Nat/Bits no longer imports Primrec and no dependency cycle appears. The prior twelve-move/ofDigits review carries forward.

Nonblocking body correction: item1 still names Nat/Bits as the Primrec theorem’s home; its actual home is now Nat/Primrec. Author’s local validation is retained. Updated after CI: exact-head CI40074728351, job120815540866, is SUCCESS across all six gates and the tidy statement ratchet. The live head is unchanged. Prior mathematical review carries forward; no new full local build is claimed. Ready under the coordinator’s integration order; the body-path correction is nonblocking.