Replace silent admit on reconstruction failure

[felipeperet]

Goal: When proof reconstruction fails to close a goal, Blaster should report a clear diagnostic instead of silently admitting it.

Obs: proveByProofStack (Blaster/Command/Tactic.lean) falls back to g.admit when neither the proof stack nor refl closes the goal, emitting only a declaration uses 'sorry' warning.

DoD:

• On reconstruction failure, Blaster surfaces a clear, visible diagnostic identifying the unclosed goal, instead of a silent admit.

[felipeperet]

#211