[performance] Constructor choice hoisting creates exponential contexts for independent fields

## Problem

On the reviewed beta stack at `36c3a15a9fdc9f3237ad376f8d67665e3742d3f8`, independently conditional fields of a constructor are lifted into an outer decision tree. A list of twelve independently chosen bits creates 16,379 optimization contexts and 117,084 hash-cons entries. The input has twelve independent choices and a compact representation with one choice per element.

This is a preparation/normalization growth issue, separate from SMT text expansion in #231. It is a small reproducer relevant to the larger `#prep_uplc` investigation in #138. I checked the open PRs: #160 addresses ancestor cache reuse and retention, not this constructor-distribution policy. #77 contains tests for the propagation rule itself; the concern here is its cost when applied indiscriminately.

## Minimal reproducer

Run this as a native Lake test module importing `Tests.Utils`:

```lean
import Tests.Utils
open Lean Meta Elab Command

run_cmd liftTermElabM do
let e ← Tests.parseTerm (← `(
fun (a b c d e f g h i j k l : Bool) =>
[if a then (1 : Nat) else 0, if b then 1 else 0,
if c then 1 else 0, if d then 1 else 0,
if e then 1 else 0, if f then 1 else 0,
if g then 1 else 0, if h then 1 else 0,
if i then 1 else 0, if j then 1 else 0,
if k then 1 else 0, if l then 1 else 0]))
let (_, env) ← Blaster.Optimize.command default e
IO.println s!"hashcons={env.optEnv.hashConsCache.size} contexts={env.optEnv.options.nextCtxId}"
```

Reducing the example to 4 and 8 binders/elements gives:

| Independent choices | Hash-cons entries | Allocated context counter |
|---:|---:|---:|
| 4 | 2,517 | 75 |
| 8 | 9,375 | 1,027 |
| 12 | 117,084 | 16,379 |

These are deterministic structural counts from Lean 4.24.0 on Apple M2 Max; no solver is invoked. Timing is deliberately omitted from this reproducer.

## Candidate direction and validation requirement

Allow choices to remain inside constructor fields, with reduction driven by the consuming function, or use a cost-aware distribution policy. Simply disabling all constructor hoisting is not a safe default performance recommendation: an isolated prototype makes SellNFT/Governance preparation much cheaper but increases subsequent proof work and slows the CIP-153 global preparation. A fix must check the residual's usability, positive properties, and expected counterexamples in addition to preparation time.

The fixing PR should include `Issue.lean` with `#testOptimize` checks for compact constructor choices and their consumers, plus a bounded structural-growth regression.

Start by running the native Lake reproducer importing Tests.Utils and inspect the propagation tests in #77 and the broader #prep_uplc investigation in #138. Add Issue.lean with #testOptimize checks for compact constructor choices and their consumers, plus a bounded structural-growth regression; done also requires checking residual usability, positive properties, and expected counterexamples.

Written by the indexing model from the issue text.