Are there non-constructive proofs of existence of "small" Turing machines / NFAs? After reading a related question, about non-constructive existence proofs of algorithms, I was wondering if there are methods of showing existence of &quot;small&quot; (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 &lt;&lt; m$), but either we can't find it at all or it'd take exponential time to compute it.
Only an extended comment with a trivial example; you can pick the one-element language:

$$L_k = \{ M \mid  \sigma(M) = \Sigma(k) \}$$

i.e. $L_k$ contains the first (in lexicographical order) busy beaver Turing machine of size $k$ (the Turing machine of size $k$ that attains the largest number of 1s on its tape after halting).

For every $k$ the language $L_k$ is regular ... but we have no idea on how to  build the small DFA that recognizes it (though it has only $\leq 2*k(\log k+2)$ states) :-)