When and what must be present on the left-hand side of the turnstile in metalogics?
Perhaps what you're missing (although you seem to suspect) is that the left hand side of the $⊢$ is not just for specifying what types variables have. In fact, as you've noted, it doesn't necessarily have all (or only) the variables on the right hand side (although in this situation it does only have variables, not things like $λy.x : α→β$).

What it's doing is keeping track of what are sometimes called the "free variables" on the right hand side, along with their specified types. The idea is essentially that there are actually no free variables in this formalism; variables are either bound by a $λ$ or in the context $Γ$. The lambda introduction rule:

$$\begin{array}{c}Γ(x:τ) ⊢ e : ρ \\ \hline Γ ⊢ λx.e : τ → ρ\end{array}$$

moves a variable from being bound in the context to being bound by a lambda. In some presentations this might even be written $λx:τ.e$ to still be explicit about what type $x$ has, but this is not really necessary when working with a derivation where the type is already recorded in the judgment (and there are other situations as well).

Of course, variables can go in the context even if they don't occur on the right hand side, like $y$ in your example. This allowed writing a constant function that doesn't actually use its argument.

One way to think about this is to read the tree bottom to top. We want to verify that $λx.λy.x$ has type $α→β→α$. The way we do this is to start in the empty context, and move upward. We use the lambda introduction rule to push lambda-bound variables into the context with an appropriate type, and eventually verify that $$x:α,y:β⊢x:α$$ holds. This is maybe more obvious if the variable rule has a line above it, allowing you to create a completed tree:

$$\begin{array}{c}\\
  \hline x:α,y:β⊢x:α \\ 
  \hline x:α ⊢ λy.x : β→α \\
  \hline ⊢ λx.λy.x : α→β→α
  \end{array}
$$

The root of the tree is our goal at the bottom, and the leaves at the top are all empty lines. $Γ$ is the local context in which we are verifying the inner parts of the lambda term, and its content is actually motivated by wanting to move under the lambda and verify the type of its body; it contains the variables and their types that have been brought into scope in that process.