Kernel-check the reconstruction gate and transport hypothesis proofs

**Goal:** Make `#testOptimize [ ..., proof ]` reject terms the kernel rejects, and make the hypothesis-driven emissions produce well-typed terms. Today the gate reports `proof ✓` on statements that `by blaster` fails with `(kernel) application type mismatch`.

**Scope:**
```
Gate (replayProofStack in Tests/Utils.lean):
- run Meta.check on the assigned proof before reporting success
- close a goal reduced to True with True.intro instead of blasterProven (proveByProofStack)
Transport (hypothesis-driven emissions, Bool / Prop / Nat / Int):
- the proof comes from hypothesisMap, keyed by the optimized binder type, while the replay substitutes the goal fvar with the original type, so the step is ill-typed whenever the hypothesis is not in optimizer normal form.
```

**DoD:**
- [x] The gate rejects the ill-typed cases (green today).
- [x] The cases close with `by blaster` and `#print axioms` shows no `blasterProven`.
- [x] Full `testOptimize` test suite with proof reconstruction green, no flag removed.