I am looking for the source and/or proper definition for the int() function
int(x) is not a function but another way to perform an explicit cast of x to an int. It is part of the C++ language itself, that is why you could not find it in a library.

This is not Arduino-specific.

In C and C++ you can cast a value to an int by doing this:

int y = (int) x;


C++ has extended this notation by allowing to do it this way, which is equivalent:

int y = int(x);


You can find this in more details in C++ language reference.