assert (forall i, j :: 0 <= i <= j <= end==>monotonic(arr,i,j)==>j-i<=endFinal-startFinal)by{
                        for i := 0 to end {
                            for j := i to end {
                                if monotonic(arr, i, j) {
                                    assert j - i <= endFinal - startFinal; // Ensures largest condition
                                }
                            }
                        }
                    }

Even though Dafny verifies the for loop, it will not verify the forall statement. Why could this be? Are they not logically equivalent?

The logical meaning of the forall statement and the for loop should be the same. So if dafny can verify one, it should be able to verify the other.