Add formally-verified refactored SMT encoder for Core

[amanda-zx]

Add a refactored SMT encoder (ProofObligation → SMT, VerifiedSMTGen/SMTEncoder.lean) with a machine-checked, sorry-free soundness proof, wired behind a new VerifyOptions.useRefactoredEncoder flag (default off).

Structure — a three-language pipeline under Languages/Core/VerifiedSMTGen/, each layer with typing + denotational semantics and order-aware well-formedness:
ProofObligation (ProofObligation.lean)
→ CoreCtx (CoreCtx.lean)
→ SMTQuery (DL/SMT/DenoteTypedSMTQuery.lean)
proved as two phase-soundness results composed into the headline
Core.Refactor.obligation_valid_of_unsatWithNegObl (EncoderSound.lean), stated
against the runtime entry point encodeObligationRun:
collect (collect_WF, collect_valid) ProofObligation → CoreCtx
translate (translateQuery_WF, query_valid_of_unsatWithNegObl) CoreCtx → SMTQuery
Shared encoder-aware name-hygiene WF lives in SharedWF.lean so the two phase
files are siblings.

Also prove the dual verdict: SMTQuery.UnsatWithObl ⟹ ProofObligation.Unsat (obligation_unsat_of_unsatWithObl), sharing the model-transfer core with the validity direction — a solver unsat on the positively-asserted goal means the obligation can never hold under its assumptions.

Semantics: SMTQuery.checkSat existentially quantifies the sort interpretation and array theory (∃σ ∃𝒜) — UnsatWithNegObl = ¬checkSat matches solver unsat. CoreCtx is self-contained, so translate is a pure CoreCtx → SMTQuery function requiring neither a TypeFactory nor a Factory.

Verified fragment (stated as WF preconditions, upgradable): restricted types — the base types bool/int/string/bitvec and arrow types over them for variables, functions, and subexpressions — datatype-free, monomorphized factory, and a subset of the predefined Core operations.

DL/SMT: add SMT-generic lemmas (typeCheck monotonicity, denoteTyped value/congruence lemmas, base-sort witnesses) in DenoteTypedProps, plus DenoteTypedFactoryCorrect (typed-Factory smart-constructor correctness).

Prove Strata.Name.disambiguate_injective (previously an unproven hypothesis), which the fresh quantifier-binder naming in translate soundness relies on.

Soundness: the soundness theorems are sorry-free, resting on the standard logical axioms (propext, funext, the Classical choice family). Three operator-name lemmas in TranslateSound — predefinedOp_typeChecks, predefinedOp_sound, and ne_reLoop_of_corePredefinedOpToSMTOp_none — each discharge the single fact CoreOp.ofString "Re.Loop" = CoreOp.re .Loop by native_decide, which runs the compiled parser and trusts the result rather than producing a kernel-checked term.

Tests (StrataTest/Languages/Core/Tests/VerifiedSMTGen/): NonVacuityTest shows the WF preconditions are non-vacuous — a concrete obligation over a real factory satisfies ProofObligation.WF/ Factory.SimpWF and the headline fires on it; DifferentialTest checks the refactored encoder against production (flag off vs on) by SMT-text diff and solver-verdict parity over a corpus of Core programs.