Let α be the least countable ordinal such that there is no polynomial-time computable recursive well-ordering of length α.

α=ωCK1, which makes the claim you made about it vacuous.

Proof: Let ⪯ be any computable well-ordering of N. Let f(n,m) be the number of steps it takes to compute whether or not n⪯m. Let g(n):=maxm≤nf(n,m) (notice I’m using the standard ordering ≤ on N, so this is the maximum of a finite set, and is thus well-defined). g is computable in O(n⋅g(n)) time. Let (,):N2→N be a bijective pairing function such that both the pairing function and its inverse are computable in polynomial time. Now let ~⪯ be the well-ordering of N given by (n,g(n))~⪯(m,g(m))⟺n⪯m, n~⪯(m,g(m)) if n is not (k,g(k)) for any k, and n~⪯m⟺n≤m if neither n nor m is of the form (k,g(k)) for any k. Then ~⪯ is computable in polynomial time, and the order type of ~⪯ is ω plus the order type of ⪯, which is just the same as the order type of ⪯ if that order type is at least ω2.

The fact that you said you think α is ω2 makes me suspect you were thinking of the least countable ordinal such that there is no recursive well-ordering of length α that can be proven to be a recursive well-ordering in a natural theory of arithmetic such that, for every computable function, there’s a program computing that function that the given theory can prove is total iff there’s a program computing that function in polynomial time.

α=ωCK1, which makes the claim you made about it vacuous.

Proof: Let ⪯ be any computable well-ordering of N. Let f(n,m) be the number of steps it takes to compute whether or not n⪯m. Let g(n):=maxm≤nf(n,m) (notice I’m using the standard ordering ≤ on N, so this is the maximum of a finite set, and is thus well-defined). g is computable in O(n⋅g(n)) time. Let (,):N2→N be a bijective pairing function such that both the pairing function and its inverse are computable in polynomial time. Now let ~⪯ be the well-ordering of N given by (n,g(n))~⪯(m,g(m))⟺n⪯m, n~⪯(m,g(m)) if n is not (k,g(k)) for any k, and n~⪯m⟺n≤m if neither n nor m is of the form (k,g(k)) for any k. Then ~⪯ is computable in polynomial time, and the order type of ~⪯ is ω plus the order type of ⪯, which is just the same as the order type of ⪯ if that order type is at least ω2.

The fact that you said you think α is ω2 makes me suspect you were thinking of the least countable ordinal such that there is no recursive well-ordering of length α that can be proven to be a recursive well-ordering in a natural theory of arithmetic such that, for every computable function, there’s a program computing that function that the given theory can prove is total iff there’s a program computing that function in polynomial time.

Thanks for the clarification. Possibly that reduces the interest of the observations about computational complexity.