Bool-not/decide bridge and nominal-decide residuals

**Goal:** Emit proof steps for the Bool-not-over-decide bridge (`optimizeBoolNot` in `OptimizeBoolNot.lean`) and close the genuinely nominal `decide` residuals in `NominalDecide.lean`. Note: `optimizeDecideCore`'s four base rules already emit, and its simple cases (`decide False/True`, `decide (nil = [..])`, `decide (P ∧ False)`) already reconstruct.

**Scope:**
```
!(decide' e) ==> decide' (¬ e)
decide p inst ==> decide' p
true = decide' e ==> e
false = decide' e ==> ¬ e
decide' e1 = decide' e2 ==> e1 = e2
decide' e1 = e2 | e2 = decide' e1 ==> e1 = (true = e2)
DecidableUpdate regrouping and the no-op Unchanged nominal cases
```

**Out of scope:**
- the BEq bridge (`beqToEq?`) inside `optimizeDecideEq`, and the acceptance of the `DecideEq.lean` suite.
- the Bool `&&`/`||` cases with a decide of a tautology/contradiction operand, e.g. `(b ∧ ¬ b) && a ==> False` (composition of Bool-binary with decide-core; if the pieces emit but do not compose on replay, that is a reconstruction-audit item).
- the decide' `&&`/`||` regrouping, and the prop-to-bool bridge (`propExprToBoolExpr?`).

**DoD:**
- [x] The bridge and the DecidableUpdate / Unchanged nominal cases push their proof step.
- [x] A `#testOptimize [ ..., proof ]` test exercises each, wired into `Tests/Optimize.lean`.
- [x] Every reconstructing in-scope test in those two files carries the `proof` flag.