" The backend sends a CopyOutResponse message to the frontend, followed by zero or more CopyData messages (always one per row), followed by CopyDone"
probably "always one per row" would be changed to note that json array format outputs two extra rows for the start/end bracket.
Fair, I was ascribing much more semantic meaning to this than it wants.
I don't see any real requirement, given the lack of semantics, to mention JSON at all. It is one CopyData per row, regardless of the contents. We don't delineate between the header and non-header data in CSV. It isn't a protocol concern.
But I still cannot shake the belief that using a format code of 1 - which really could be interpreted as meaning "textual csv" in practice - for this JSON output is unwise and we should introduce a new integer value for the new fundamental output format.