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.
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.