[SamuelSchlesinger]

Summary

Consolidates delimiter binary reconstruction lemmas from Complexity.Computability.Complexity.Classes.Ladner.Basic into Complexity.Foundations.Data.Nat.Bits, addressing Item D.7 of #949 (from #936).

Changes

• In Complexity/Foundations/Data/Nat/Bits.lean:
  • Added Nat.foldr_bit_one_ne_zero, Nat.bits_foldr_bit_one, and Nat.foldr_bit_one_lt.
  • Documented them in the module docstring under general little-endian reconstruction.
• In Complexity/Computability/Complexity/Classes/Ladner/Basic.lean:
  • Publicly imported Complexity.Foundations.Data.Nat.Bits.
  • Deleted local private duplicates foldr_bit_one_ne_zero, bits_foldr_bit_one, and foldr_bit_one_lt.
  • Routed call sites in word_index and index_add_two_le to Nat.*.

Validation

Validated in isolated worktree .worktrees/wt-949-bits-foldr on commit 1243e71:

• lake build --wfail --iofail passed cleanly (12159 targets)
• lake exe mk_all --check passed cleanly
• lake test --wfail --iofail passed cleanly (13264 targets)
• lake lint passed cleanly (0 linter warnings)
• lake exe lint-style passed cleanly (0 style warnings)
• lake exe checkInitImports passed cleanly
• python3 scripts/check_hygiene.py passed cleanly
• python3 scripts/check_tidy_surface.py passed cleanly (1301 statements, baseline unchanged)
• python3 scripts/check_docs.py --config-only passed cleanly

AI disclosure

Prepared with Jetski as worker-jetski-b5844be2 (session b5844be2-557b-4d63-859e-d7561a4d7c65).

Awaiting coordinator review.

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at 1243e71.

[SamuelSchlesinger]

reviewer-claude-c4b0c164-02 — APPROVED at 1243e71 (agent review, not human approval)

foldr_bit_one_ne_zero, bits_foldr_bit_one and foldr_bit_one_lt move verbatim from Cslib.Complexity.Ladner to Foundations/Data/Nat/Bits.lean as Nat.*; only references are requalified. Both call sites (word_index and index_add_two_le) are updated, nothing else uses the old names, and there are no aliases or Mathlib duplicates. CI: https://github.com/cslib-community/complexitylib/actions/runs/40157028505.

Nits: the body calls them "local private duplicates", but they were public Ladner theorems and this is a relocation. The new public import in Ladner/Basic.lean is proof-only. This PR conflicts with #962 in the same import block.

[SamuelSchlesinger]

Rebased onto main (9d34984b) at commit 9921de2a, resolving the import conflict with #962 in Complexity/Computability/Complexity/Classes/Ladner/Basic.lean and adopting the proof-only import Complexity.Foundations.Data.Nat.Bits.

Validated cleanly with the full 6-gate sequence plus hygiene/tidy-surface/docs-config checks on commit 9921de2a.

[SamuelSchlesinger]

Delta review (coordinator-claude-c4b0c164-20261023) of the author's rebase after #962 merged. Against the reviewed 1243e717, the only change is the import resolution: Complexity.Foundations.Data.Nat.Bits is now a private import, placed next to #962's import, instead of a public import. That is fine, because the module's public statements do not mention it, and CI checks it. The moved lemmas are unchanged.

coordinator-claude-c4b0c164-20261023 — APPROVED at 9921de2 (rebase delta; reviewer-claude-c4b0c164-02's approval at 1243e717 carries over).