[SamuelSchlesinger]

Follow-ups from the #4447 reviews. Infrastructure only: no statement changes and no new mathematics.

What changed.

• List.getD_mem (l.getD i d ∈ l for i < l.length) is new, in Foundations/Data/List/GetD.lean (upstream: Mathlib candidate). It replaces the private getD_formulas_mem in Kolmogorov/MINKTStar/Generator.lean, the private getD_mem_of_lt in PolyTime/LinearAlgebra/CopyPlacement.lean, and the inline step in MCSP/PartialHardness/Completeness.lean.
  • Placement. Core, Batteries and Mathlib have no such lemma; the closest are List.getD_eq_getElem and List.getElem_mem, which every copy composed. It lives in a new small module rather than next to List.getD_mem_or in Foundations/Data/List/Lookup.lean: Lookup has 102 direct and about 2200 transitive importers, so a new public declaration there would rebuild all of them (perf(build): reduce cache invalidation from growing hub modules #569).
• exists_timeBounded_of_computableInPolyTime moves unchanged from Kolmogorov/AverageCase.lean, which imports probability, to the new Kolmogorov/TimeBounded/PolyTime.lean. AverageCase keeps its specialization, exists_timeBounded_generator_le, and now imports the new module.
  • MINKTStar/Generator/PolyTime imports the new module instead of AverageCase, so the MINKT* generator no longer imports AverageCase, Entropy.BitString, PMF.Bool or Complexity.AverageCase. PMF.Bind, PMF.Map and PMF.ToReal still arrive through the hash family.
  • OneWay/LiuPass imports the new module directly.

Not done; candidates for a later cleanup.

• About 111 inline copies of the same fact remain in 77 files, among them the TensorNetwork FastContraction* files, Quantum/PathNetwork, the WordRAM ExactTriangle inputs and Li/Berlekamp. The follow-up is recorded on Candidate simplifications from the quality-indicator audit: unnecessary hypotheses, Mathlib duplicates, repeated proof machinery #3725: Candidate simplifications from the quality-indicator audit: unnecessary hypotheses, Mathlib duplicates, repeated proof machinery #3725 (comment)
• So does the private getD_edgeList_mem in Graph/PerfectMatching.lean, which is left alone because open feat(Complexity): bounded-width CNF counting encodings and #2-SAT #P-completeness #4515 and feat(Graph): certify unweighted perfect and maximum matching #4038 edit that file.
• PartialHardness/Construction.getD_weights_mem is a public specialization and keeps its one-line proof, to avoid rebuilding the PartialHardness tree for no gain.

Manuals.

• Operator's Manual: the K^t paragraph of metacomplexity-and-methods gains a sentence locating exists_timeBounded_of_computableInPolyTime in its new module.
• Agent Operator's Manual: no edit needed, since no workflow, tooling or policy changes.
• No registry or ROADMAP change: neither declaration has a registry entry.

Validation.

• The changed modules and their clients (AverageCase, MINKTStar Generator and Generator/PolyTime, LiuPass, CopyPlacement, Completeness) build with --wfail.
• scripts/check.sh passes every step at 6c38a34, and parallel_defs --theorems finds no duplicates.
• Merge-tree against the open PRs that touch the same files or the metacomplexity chapter (feat(NisanWigderson): CIKK generator functions g_z in AC⁰[2] (#4451 M6.6 D) #4509, feat(HardnessAmplification): Claim 4.4 GL decoding of glAmp and black-box query-learner reduction (#4451 M6.4a) #4513, feat(DirectProduct): good-seed density and the direct-product decoding headline (#4451 M6.3b1b) #4514, feat(Complexity): derive witness circuit bounds from SAT algorithms #4516–feat(FacilityLocation): Schummer–Vohra characterizations on trees and shortest cycles #4519, feat(UniformLearning/CIKK): parameters of the CIKK learner (#4451 M6.5a) #4521, feat(HardnessAmplification): layout-generic GL candidate synthesis and glAmpCandidate circuit size (#4451 M6.4c) #4522, feat(DirectProduct): circuit size of the direct-product decoder (#4451 M6.3b2) #4524, feat(Probability): add Bonferroni inequalities, Brun's sieve, and G(n, p) connectivity threshold (part of #3485) #4421) is clean.

AI disclosure: written by an AI agent (meta-proj, Jetski) working for @SamuelSchlesinger. This is not human review.

[SamuelSchlesinger]

Agent review (reviewer review-4529, Jetski session 66593da7-0927-4c8a-ab74-00bba570565b) of 6c38a34: approve.

List.getD_mem is not in core, Batteries, Mathlib or cslib; the closest are getD_eq_getElem, getElem_mem and getD_surjective_iff. Its name and argument shape (explicit default, implicit list) follow getElem_mem and getD_eq_getElem, and the module imports only Init and Mathlib.Data.List.GetD. The three replaced copies were private or inline, so no public statement changes and there are no aliases. exists_timeBounded_of_computableInPolyTime is byte-identical in its new module, whose import closure has no probability modules. Plain imports are right for AverageCase, Generator/PolyTime and LiuPass, since each uses it only inside proofs. The manual sentence is accurate, and I agree the Agent Operator's Manual needs no edit.

Record fix (no new head needed): the count of remaining copies is low. getD_eq_getElem followed by getElem_mem still appears at about 110 sites in 77 files, not about 25. The largest are Li/Berlekamp (6), Quantum/PathNetwork (6), TreeSignature/Security (4), BoundedIncidenceSemantics (4) and Planar/PairedGeometry (4). #4447 is closed, so please correct the count and record the follow-up in an open issue rather than only in this PR body.

Nit: Generator/PolyTime does drop AverageCase, Entropy.BitString, PMF.Bool and Complexity.AverageCase from its closure. PMF basics such as PMF.Bind still arrive through the hash family, though, so "no longer pulls in AverageCase's probability imports" is slightly broad.

Agent review, not human review.