... Right. I think I've finally tracked down where the Serial buffer size is defined in the Espruino source code.

I'm leaving this step-by-step trail of breadcrumbs here in case it helps anyone else to decode the Espruino source code, and to refresh my memory if I ever need to track down chip details like this again in the future.

1. First, we know we're looking for something to do with the Serial1 port. Serial1 is an instance of the Serial class, and (as per the API documentation) that's a USART.
2. So step two is to find the Espruino source code repo (thank god for open source!) and search it for USART.
3. Hmmm - looks like there are a lot of different source code files, so let's look for one that sounds like it belongs to the chip we're using (in this case, the Espruino Pico). According to the Pico page the chip in the Pico is an STM32F401CDU6 32-bit 84MHz ARM Cortex M4 CPU.
4. Ok... so scrolling down the list of possible hits in the github repo, "stm32f4xx" looks like a pretty good match for "STM32F401CDU6. Let's look in there.
5. Hah - this looks like the header file for a C structure that represents a USART in memory. The beginning of the file sets up a struct (basically, "object" in JS-speak) that has a bunch of familiar-sounding fields like USART_BaudRate, USART_StopBits and USART_Parity that pretty obviously map to options/parameters used when setting up the Serial prot in the Espruino JS API.
6. Jackpot! Towards the bottom of the file we find the definition for a function called USART_SendData: USART_SendData(USART_TypeDef* USARTx, uint16_t Data);. That sounds very much like the bit of code that sends data down a USART, so let's jump to the associated .c file (source code) for this .h (header) file.
7. Find the USART_SendData function in this file and it's a short one that just seems to set a member variable called DR, belonging to a variable called USARTx, that's a pointer to a variable of type USART_TypeDef that's passed into the function.
8. Ok, so let's back up and find where USART_SendData() is called from, so we can find where this parameter variable comes from.
9. The first place the function is actually called (as opposed to being defined in a header file) is targets/stm32/stm32_it.c... and STM32 is a reassuring match for our chip (STM32F401CDU6), so let's look in there.
10. Search that file for USART_SendData( and we find the following likely-looking code:

/* If we have other data to send, send it */
    int c = jshGetCharToTransmit(device);
    if (c >= 0) {
      USART_SendData(USART, (uint16_t)c);
    }

So this is basically saying "get a single character from the jshGetCharToTransmit() function, and if it's not 0 then send it out over the USART". That's very good - now we just need to find jshGetCharToTransmit() and try to work out where it gets characters from so we can try to work out how big that buffer actually is.
11. src/jsdevices.c looks like a pretty good bet, so let's look in there (and search withing the file for jshGetCharToTransmit.
12. The first hit is what we want. The code is a bit confusing, but if you ignore all the if(DEVICE_IS_UART(...)) stuff then a few lines below that we find unsigned char data = txBuffer[tempTail].data;, and that variable is returned from the function. So txBuffer is our buffer that holds all outgoing data to be sent over a USART (Serialn) connection.
13. Right at the top of the file we find volatile TxBufferItem txBuffer[TXBUFFERMASK+1];, definine an array of TXBufferItems called txBuffer, of size... TXBUFFERMASK+1.
14. Sigh... ok, so now let's find out where TXBUFFERMASK is defined. Nowhere in this file. awesome.
15. At least it's only used in two files. We know it's not src/jsdevices.c because we just looked in that one, so it must be the other one, scripts/build_platform_config.py.
16. Search in that file and we find (third result) codeOut("#define TXBUFFERMASK "+str(bufferSizeTX-1)+" // (max 255)"). This looks like some Python code that writes C (always fun reading code-that-writes-code), but if I'm reading this right it means that at compile-time TXBUFFERMASK is defined as one smaller than bufferSizeTX
17. ... and bufferSizeTX is defined a few lines above as:

if LINUX:
  bufferSizeIO = 256
  bufferSizeTX = 256
  bufferSizeTimer = 16
else:
  bufferSizeIO = 64 if board.chip["ram"]<20 else 128
  bufferSizeTX = 32 if board.chip["ram"]<20 else 128
  bufferSizeTimer = 4 if board.chip["ram"]<20 else 16

Phew!

So long story short it looks like the size of the Serial output buffer is defined at compile time based on the RAM size of the chip.

18. Tracking back up the file we find that board is imported via board = importlib.import_module(boardname);, and boardname is passed in as a command-line parameter to the build. Crap.

19. Ahah - thank god for comments:

Reads board information from boards/BOARDNAME.py and uses it to generate a header file

which describes the available peripherals on the board

So let's take a look in the boards folder and see if we can spot anything that looks like our chip.

20. I don't know about you, but I have a good feeling about STM32F401CDISCOVERY.py for an STM32F401CDU6 chip, so let's look in there.

21. Booyah! I spy a chip object with a ram member with a value of 64. Plugging that into our lookup table above, board.chip["ram"] (64) is certainly not <20, which means it's defined as 128.

That makes our output buffer for serial data a surprisingly-small 128 unsigned chars big.

That seems way too small for something that only starts choking on writes of a couple of K or more, so perhaps there's another buffer somewhere, further up the stack that I've missed.