[SamuelSchlesinger]

Addresses item A.2 on #949.

Summary of Changes

• Mathlib reuse: Replaced duplicate private nat_prod_pos_iff in Complexity.Computability.Complexity.Classes.Oracle.Lowness and Complexity.Computability.Complexity.Classes.SharpP.Lowness with Mathlib's CanonicallyOrderedAdd.prod_pos.
• Public extraction: Extracted duplicate private helper ofFn_getElem_of_length_eq from both files into public lemma List.ofFn_getElem_of_length_eq in Complexity.Foundations.Data.List.Lookup.

Validation

Verified in isolated worktree wt-949-lowness:

• lake build --wfail --iofail (passed)
• lake exe mk_all --check (passed)
• lake test --wfail --iofail (passed)
• lake lint (passed)
• lake exe lint-style (passed)
• lake exe checkInitImports (passed)
• python3 scripts/check_hygiene.py (passed)
• python3 scripts/check_tidy_surface.py (passed)
• python3 scripts/check_docs.py --config-only (passed)

AI disclosure

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

[SamuelSchlesinger]

Review claimed by reviewer-claude-c4b0c164-02 (agent review) at 54af5a8.

[SamuelSchlesinger]

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

Both private nat_prod_pos_iff copies are replaced by Mathlib's CanonicallyOrderedAdd.prod_pos, which has the same statement. Both private ofFn_getElem_of_length_eq copies become the public List.ofFn_getElem_of_length_eq in Foundations/Data/List/Lookup.lean. All 5 call sites are updated, no copies remain, and there are no aliases. CI: https://github.com/cslib-community/complexitylib/actions/runs/40155084642.

Nits: the extracted lemma is generalized from List Bool to List α, which the body doesn't say. It is the core lemma List.ofFn_getElem up to subst h; a one-line proof via it would make that visible. #964 also edits Lookup.lean's Main results, so expect a trivial restack conflict.