The Base Canonicalization Theorem for Hilbert's epsilon-Calculus under Unique Satisfiability

Formal logic. AI-assistance disclosure: the base theorem (Paper I) and its hand derivation are the author's own; LLM assistance was used for proof search/derivation of the nested and n-layer extensions (Papers II/III) building on the hand-proved base, proof-engineering of the Coq/Rocq scripts and certificate tooling, drafting, and literature search. All results verified by the author and by machine checking (Rocq 9.1.1; independently reverified under Rocq/Coq 9.2). No AI system is an author. Version note: v3. Three-title lineage: Bounded epsilon-Calculus and the Survivor Witness (v1) -> Explicit and Mechanized Canonicalization under Unique Satisfiability in Hilbert's epsilon-Calculus (v2) -> The Base Canonicalization Theorem for Hilbert's epsilon-Calculus under Unique Satisfiability (v3). Related-work revision; AI-disclosure added.