# lean4-0002: kernel/inductive.cpp O(K×N) — std::find in nested loop for inductive type validation

**Target:** leanprover/lean4
**Severity:** MEDIUM
**CWE:** CWE-407 (Inefficient Algorithmic Complexity)
**MOAD:** MOAD-0001 (A Sedimentary Defect)
**File:** `src/kernel/inductive.cpp:529–532`
**Language:** C++
**Status:** open

## Description

Inside the kernel's inductive type validator, `std::find` on a plain `buffer<expr>`
runs inside a `for` loop over another buffer. For a constructor with K type-former
arguments and N result arguments, cost reaches O(K×N).

## Root Cause

```cpp
// inductive.cpp:526–532
buffer<expr> result_args;
get_app_args(type, result_args);
/* Check condition 2: every argument in to_check must occur in result_args */
for (expr const & arg : to_check) {                                        // O(K) outer
    if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())  // O(N) inner
        return true; /* Condition 2 failed */
}
```

`to_check` holds type-former arguments; `result_args` holds application
arguments from the return type. Both grow with constructor arity.

## Fix

Use `std::unordered_set<expr>` (or Lean's `expr_set`) for `result_args`:

```cpp
expr_set result_set(result_args.begin(), result_args.end());  // O(N) build
for (expr const & arg : to_check) {
    if (result_set.find(arg) == result_set.end())             // O(1) lookup
        return true;
}
```

## Related

`inductive.cpp:543` — same `std::find` pattern for fresh universe param name
generation (while loop scanning `m_lparams`). Low severity in practice since
universe parameter counts stay small, but structurally identical defect.