What are the formal conditions for a wildcard parameter in a Java generic type to be within its bounds?

With parameterized types in Java, how do the rules that check if a parameter is within its bound work exactly for wildcards?

Given a class like this:

class Foo<T extends Number> {}

Experimenting with what the compiler accepts learns that:

• A ? extends wildcard using an unrelated interface type is allowed: Foo<? extends Runnable> is valid
• A ? extends wildcard using an unrelated class type is not allowed: Foo<? extends Thread> is invalid. That makes sense because no type can be a subtype of both Number and Thread
• In a ? super wildcard, the lower bound in the wildcard must be subtype of the bound of the type variable: Foo<? super Runnable> is not allowed because Runnable is not a subtype of Number. Again, this restriction makes perfect sense.

But where are these rules defined? Looking at the Java Language Specification section 4.5, I don't see anything distinguishing interfaces from classes; and when applying my interpretation of the JLS Foo<? super Runnable> is said to be valid. So I probably misunderstood something. Here's my attempt:

From that section of the JLS:

A parameterized type consists of a class or interface name C and an actual type argument list <T1 , ... , Tn>. It is a compile time error if C is not the name of a generic class or interface, or if the number of type arguments in the actual type argument list differs from the number of declared type parameters of C. In the following, whenever we speak of a class or interface type, we include the generic version as well, unless explicitly excluded. Throughout this section, let A1 , ... , An be the formal type parameters of C, and let be Bi be the declared bound of Ai. The notation [Ai := Ti] denotes substitution of the type variable Ai with the type Ti, for 1 <= i <= n, and is used throughout this specification.

Let P = G<T1, ..., Tn> be a parameterized type. It must be the case that, after P is subjected to capture conversion (§5.1.10) resulting in the type G<X1, ..., Xn>, for each actual type argument Xi, 1 <= i <= n , Xi <: Bi[A1 := X1, ..., An := Xn] (§4.10), or a compile time error occurs.

Apply that to P = Foo<? super Runnable>: that gives C = Foo, n = 1, T1 = ? super Runnable and B1 = Number.

For capture conversion this part of the definition of capture conversion applies:

If Ti is a wildcard type argument of the form ? super Bi, then Si is a fresh type variable whose upper bound is Ui[A1 := S1, ..., An := Sn] and whose lower bound is Bi.

That gives G<X1, ..., Xn> = Foo<X> where X is a fresh type variable with upper bound Number and lower bound Runnable. I don't see anything explicitly forbidding such a type variable.

There are no type variables in B1 = Number, so Bi[A1 := X1, ..., An := Xn] is still simply Number. X has Number as upper bound (coming from the capture conversion), and according to the subtyping rules "The direct supertypes of a type variable are the types listed in its bound", so X <: Number (= Bi[A1 := X1, ..., An := Xn]), so this parameter is within its bounds. (But it isn't!)

Following the same reasoning every wildcard is within its bounds, so something here isn't right... But where exactly did this reasoning go wrong? How do these rules work when applied correctly?