Mangled nested class namein the Java Language Specification

Question

Consider the following two classes:

// a.java
public class a
{
    public static class $b
    {

    }
}

// a$.java
public class a$
{
    public static class b
    {

    }
}

Obviously, due to inner/nested class name mangling, a$.b and a.$b will both be compiled to a class file named a$$b.class. When the command javac a.java a$.java is executed, the Oracle Java compiler (javac 1.7.0_45) produces the following output:

a$.java:3: error: duplicate class: a.$b
    public static class b
                  ^
1 error

Where does it say in the Java Language Specification that these class names (a$.b and a.$b ) clash, or is this just an established convention due to the output files having the same name?

Answer 1

6.1 which points to 3.8 which says:

An identifier is an unlimited-length sequence of Java letters and Java digits, the first of which must be a Java letter.

...

The "Java letters" include uppercase and lowercase ASCII Latin letters A-Z (\u0041-\u005a), and a-z (\u0061-\u007a), and, for historical reasons, the ASCII underscore (_, or \u005f) and dollar sign ($, or \u0024). The $ character should be used only in mechanically generated source code or, rarely, to access pre-existing names on legacy systems.

(emphasis mine)

Though really, it's just a matter of you having a duplicate class name after bytecode generation. The same error would occur with two colliding class names that didn't involve $ in the source.

Edit to add: The binary format is specified in 13.1