Confirmation of alternative correctness proof for Floyd-Warshall's all-pair shortest-path algorithm
Your effort towards a new kind of proof for Floyd-Warshall algorithm is appreciated.

On one hand, your proof is very well written. It cannot be said to be all wrong as apparently you have tried to avoid saying anything wrong.

On the other hand, I would not call you proof a proof that is different from the usual induction proof on the loop variable of the outer-most loop.


  ... $p_m$ has the biggest index in the matrix, meaning that the algorithm would have already correctly found the length of $P_1$ and $P_2$ and stored them in $d_{i_{p_m}}$ and $d_{p_{m_j}}$, since they share intermediate vertices of smaller index and therefore would have been found in previous iterations of the outer-most loop.


Take a moment to reflect. What you said above is basically the induction hypothesis in the usual induction proof on the loop variable of outer-most loop. That induction hypothesis can be viewed as a proposition that is even stronger than the final result of the Floyd-Warshall algorithm. Armed with that kind of knowledge, it is expected the correctness can be proved easily. In other words, it is not far fetched to say you just proved its correctness by admitting its correctness. Or, you just repeated the usual proof with some extra unnecessary logic.

There is another hidden flaw in your proof that is actually critical. Suppose there is a negative cycle in a connected graph. Floyd-Warshall algorithm handles that situation graciously. However, there is no shortest paths between any pairs of vertices in the graph, since given any path, you can always find another path that is shorter. So, your induction hypothesis becomes void in that case.