[correctness] Shared substitution mishandles argument slices and captures open replacements

The shared substitution helpers on `beta-lambda-cache-optimization` (`bafdd4f7`) disagree with Lean's native substitution for nonzero argument slices and for open replacements under binders.

Minimal reproducer:

```lean
import Blaster.Optimize.Env.Instantiate
open Lean Meta Elab Command Blaster.Optimize
run_cmd liftTermElabM do
let check : TranslateEnvT Unit := do
let e ← hashcons (.bvar 0)
let args ← (#[mkRawNatLit 10, mkRawNatLit 20] : Array Expr).mapM hashcons
let actual ← instantiateSharedRevRange e 1 2 args
unless actual == e.instantiateRevRange 1 2 args do
throwError "expected 20, got {repr actual}"
check.run' (default : TranslateEnv)
```

Actual: `bvar 0`. Expected: literal `20`. `beginIdx` selects a slice of the substitution array; it does not shift the bound-variable cutoff.

A second minimal case substitutes `bvar 0` into `fun y : Nat => bvar 1` using `instantiateShared1`: the result captures the replacement as `fun y => bvar 0`, whereas native substitution lifts it to `fun y => bvar 1`. `betaLambdaSharedRange` also instantiates from array offset zero instead of its requested beginning.

These are helper correctness defects. Most observed production callers use closed arguments and slices starting at zero; a false top-level Blaster theorem has not been established from these cases. The fix should compare against native substitution across expression constructors, depths and slices, and include ordinary optimizer beta-reduction regressions in the numbered issue test.

Start with the shared substitution helpers exposed by Blaster.Optimize.Env.Instantiate: instantiateSharedRevRange, instantiateShared1, and betaLambdaSharedRange. Compare them with Lean's native substitution across expression constructors, binder depths, open replacements, and argument slices, then add the requested numbered issue test and ordinary optimizer beta-reduction regressions.

Written by the indexing model from the issue text.