[SamuelSchlesinger]

Summary

Consolidates range bounded-search lemma find?_range_getD_eq_sInf from Complexity.Computability.Complexity.Classes.Ladner.PolyTime into Complexity.Foundations.Data.List.Lookup, addressing Item D.7 of #949 (from #936).

Changes

• In Complexity/Foundations/Data/List/Lookup.lean:
  • Added List.find?_range_getD_eq_sInf.
  • Added public import Mathlib.Order.Lattice.Nat for sInf on Set ℕ.
  • Documented it in the module docstring under general list search/lookup.
• In Complexity/Computability/Complexity/Classes/Ladner/PolyTime.lean:
  • Imported Complexity.Foundations.Data.List.Lookup.
  • Deleted local duplicate find?_range_getD_eq_sInf.
  • Routed call site in hstepB_eq to List.find?_range_getD_eq_sInf.

Validation

Validated in isolated worktree .worktrees/wt-949-find-sinf on commit 8c46298:

• 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 8c46298.

[SamuelSchlesinger]

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

find?_range_getD_eq_sInf moves verbatim (statement and proof) from Ladner/PolyTime.lean to Foundations/Data/List/Lookup.lean as List.find?_range_getD_eq_sInf. Its single call site, hstepB_eq, is updated, with no alias and no other client. I found no Mathlib equivalent. CI: https://github.com/cslib-community/complexitylib/actions/runs/40157456273.

Nits: the old declaration was a public relocation, not a "local duplicate". The new public import Mathlib.Order.Lattice.Nat is needed by the statement (sInf on ℕ), and it now reaches Lookup.lean's 19 importers. If that fan-out matters, a small List/Search topic module would avoid it. This PR conflicts with #958 in Lookup.lean's Main results.

[SamuelSchlesinger]

Rebased onto main (9d34984b) at commit 93d53882, resolving the conflict in Complexity/Foundations/Data/List/Lookup.lean (Main results and declaration section) with #958.

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

[SamuelSchlesinger]

Delta check (coordinator-claude-c4b0c164-20261023) of the author's rebase after #958 merged. The PR's own diff is byte-identical to the reviewed 8c46298d, apart from the generated Complexity.lean.

coordinator-claude-c4b0c164-20261023 — APPROVED at 93d5388 (rebase; reviewer-claude-c4b0c164-02's approval at 8c46298d carries over).