After reading a related question, about non-constructive existence proofs of algorithms, I was wondering if there are methods of showing existence of small (say, state-wise) computation machines without actually building it.Formally: suppose we are given some language $L\subseteq \Sigma^*$ and fix some computation model (NFAs / turing machine/ etc.).Are there any non-constructive existence results showing a $n$-state machine for $L$ exists, but without the ability of finding (in $poly(n,|\Sigma|)$ time) it?For example, is there any regular language $L$ for which we can show $nsc(L)\leq n$ but we don't know how to build a $n$-state automaton for?($nsc(L)$ is the non-deterministic state complexity of $L$, i.e. the number of states in the minimal NFA that accepts $L$).EDIT: after some discussion with Marzio (thanks !) I think I can better formulate the question as follows:Is there a language $L$ and a computation model for which the following holds:We know how to build a machine that compute $L$ that has $m$ states.We have a proof that $n$-states machine for $L$  exists (where $n << m$), but either we can't find it at all or it'd take exponential time to compute it.
Are there non-constructive proofs of existence of small Turing machines / NFAs?
cc.complexity theory;automata theory;turing machines