A helper whose value depends on a hole is emitted into `ChallengeDeps`, so the workspace cannot build

Summary

generate splits a problem's same-module dependencies into holes and helpers,
and emits every helper into ChallengeDeps.lean. But ChallengeDeps is
imported beneath the hole layer, so holes are not in scope there. A helper
whose value mentions a hole ends up calling an identifier that is not in the
module it lands in, and the workspace does not compile.

The shape that triggers it

/-- hole -/
@[eval_problem]
theorem exists_pos : ∃ n : Nat, 0 < n := by
  sorry

/-- NOT a hole; its value consumes the hole's proof -/
noncomputable def witness : Nat :=
  Classical.choose exists_pos

/-- hole; its statement mentions `witness` -/
@[eval_problem]
theorem witness_pos : 0 < witness := by
  sorry

with both theorems in the manifest's holes. generate classifies witness as
a helper, so the emitted ChallengeDeps.lean is:

import Mathlib

namespace ToyHoleDep

noncomputable def witness : Nat :=
  Classical.choose exists_pos

end ToyHoleDep

error: ChallengeDeps.lean:9:19: Unknown identifier `exists_pos`

This shape is not avoidable by authors: Classical.choose : (∃ x, p x) → α
turns a proof into data, which is how the mathematics is usually written --
prove existence, then define the object it produces.

Where it happens

EvalTools/Generate.lean, building helperNames:

let holeNames : Std.HashSet String :=
  extracteds.foldl (init := {}) fun acc e => acc.insert e.declarationName
let helperNames : Std.HashSet String :=
  extracteds.foldl (init := {}) fun acc e =>
    e.sameModuleDependencies.foldl
      (fun a n => if holeNames.contains n then a else a.insert n) acc

The filter drops dependencies that are holes, but keeps dependencies that
depend on holes.

Why the manifest cannot work around it

• non-hole — stays in ChallengeDeps, cannot compile;
• definition hole — type pinned, body free, so a solver supplies any Nat
  and the author's construction is lost;
• theorem hole — same loss, and it is not Prop.

The declaration needs its data frozen and a position below the hole layer.

Suggested fix

Make hole-dependence transitive when partitioning, and emit anything at or below
the cut into the hole layer instead of ChallengeDeps:

ChallengeDeps.lean     no transitive dependency on a hole
Challenge/Submission/Solution.lean     the holes, plus everything downstream

The moved declarations are not turned into holes -- they stay out of
theorem_names and definition_names, so the comparator still compares them by
full ConstantInfo and the data stays frozen.

Start in EvalTools/Generate.lean at the helperNames partitioning logic, then reproduce the reported workspace build with the exists_pos/witness shape. Trace same-module dependencies transitively and verify that ChallengeDeps.lean contains no declaration depending on a hole, while Challenge/Submission/Solution.lean contains downstream declarations unchanged and the workspace compiles.