feat: add `Environment.realizationEnvContains`

This PR adds `Environment.realizationEnvContains forConst c`, which reports whether `realizeConst forConst` callbacks can access `c`. This is the criterion for choosing `forConst` when a realization depends on multiple constants: the target must be one whose realization environment contains all others.

The realization environment of a local constant is the snapshot taken by `enableRealizationsForConst`, so it contains the declarations added before that call, including the other declarations of its mutual block and asynchronously elaborated theorems; for imported `forConst` it is the import environment. The `realizeConst` docstring now points to the new accessor. The realization context lookups now use `Environment.isImportedConst`, which moves above `enableRealizationsForConst` together with `getModuleIdxFor?`.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>