On 5.5.6 and 5.4.26 which I have currently available, output is the same as in the manual. Could you provide exact code which gave you result with those characters lowercased?

I'm sorry, it is in fact a bug in the program and not in the documentation.

You are right that < and > are encoded in upper case, but they are the only ones that behave so !

See that program :

<?php
$json_string = '{
        "ctrl1" : "\\u000B\\u000E\\u000F",
        "ctrl2" : "\\u001B\\u001C\\u001D\\u001E\\u001F",
        "other" : "<> élève grâce à 北京"
}';
$json_value = json_decode($json_string);
$json_string2= json_encode($json_value, JSON_HEX_TAG | JSON_PRETTY_PRINT);
echo var_dump($json_string2);
?>

The display is :
string(160) "{
    "ctrl1": "\u000b\u000e\u000f",
    "ctrl2": "\u001b\u001c\u001d\u001e\u001f",
    "other": "\u003C\u003E \u00e9l\u00e8ve gr\u00e2ce \u00e0 \u5317\u4eac"
}"

As you can see, the control characters are \u000b to \u001f, the French accented letters are \u00e0 to \u00e9, and the second chinese character is \u4eac, all in lower case. Only < and > are \u003C and \u003E in upper case.

Note: In JavaScript, the JSON.stringify function also encodes the control characters in lower case; I don't know how to obtain hexadecimal code for characters above \u001f.

It probably needs futher clarification. I'll try to expand this example to show behavior you've described.

Ok, and thank you!