perf(ixvm): share argument-independent substitution work

[arthurpaulino]

Large beta-reduction traces repeatedly instantiate the same expression with different arguments even when most subtrees do not reference the substituted binders. Those calls have distinct memo keys, so the kernel previously rebuilt the same argument-independent subtrees for every application.

Add an exact loose-BVar occurrence query for single substitution. When the target binder is absent, lower only the higher variables through the existing memoized lowering path. Apply the analogous range test to simultaneous substitution: if no binder in the substitution window occurs, lower the expression once without keying the result on the substitution list. The ordinary substitution walks remain unchanged whenever an argument is actually used.

Keep the resulting hot lowering circuit narrow by extracting its BVar, binder, and let arms into cold helpers. This is a circuit-layout change only; it reduces expr_lower_walk from width 53 to 34. Regenerate the native IxVM kernel.

Validation:

• A native sweep passed all 600 Init, InitStd, Batteries, Lean, FLT, and Mathlib shards without errors or timeouts.

• Total FFT cost fell from 258.065T to 248.348T (-3.77%); Mathlib fell 5.12% and FLT fell 3.82%.

• The former worst Mathlib shard fell from 1.740T to 1.206T (-30.66%), with elapsed time dropping from 260.67s to 187.68s and peak RSS from 38.76M KiB to 29.48M KiB.

• On the next dominant isolated constant, CoalgCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right, the lowering circuit split further reduced FFT from 123.664B to 118.932B (-3.83%). Its left/composite siblings and the established Init, Batteries, and Nat.add_comm guards all pass under bytecode interpretation.