Invariant Proof of For Loops?
The loop invariant probably involves the loop control variable.  If so, it only makes sense to ask if the invariant is true, when the loop control variable is initialized. When the loop control variable is uninitialized, expressions that involve it are undefined.

Consider a simple example, a loop whose purpose is to determine whether all the elements of a (0-based) array $a$ are equal:

   all_equal = true
   for (i = 1; i &lt; a.size; i++)
      if a[i-1] ≠ a[i] 
         all_equal = false


Here the loop invariant is that $all\_equal$ is true if and only if the $a[k]$ are all equal for each $k$ with $0 \le k \le i$.

This is makes no sense at all unless the loop control variable $i$ has a well-defined value.  Before the initialization, it doesn't. After the initialization, we have $i=1$, and the loop invariant is true.