Proof for LeetCode: 11. Container With Most Water problem

UPDATE: I abandoned this initial approach in favor of a more powerful invariant I worked out after posting. I've detailed that one in an answer below.

I'm new to algorithm correctness proof-writing but am keen to improve my skill there.

I have a first attempt here, but I think I'm missing a final step. The algorithm is for
the LeetCode: 11. Container With Most Water problem.

I've shown to my satisfaction that only an "advance the lesser" move at any given point
can possibly result in a greater area (water volume), but it feels like I'm missing the
part where I can say "therefore this algorithm will always find the maximum".

Any pointers on process, notation, or formalisms is also greatly appreciated. This proof
strikes me a bit as "workshop-grade" and I wouldn't mind getting a bit more elegant
about it as I do others.

Problem Statement:

Given an array of non-negative integers hs (heights) where each represents a point at
coordinate (i, hs[i]), n vertical lines are drawn such that the two endpoints of line
i is at (i, hs[i]) and (i, 0). Find two lines, which together with the x-axis form
a container, such that the container contains the most water.

Notation:

• H - Height

• W - Width

• A - Area

|--W--|

       |           ___  
       |     |      |
       |  |  |  |   H
    |  |  |  |  |   |
    +--+--+--+--+  ---
    0  1  2  3  4

For example, a maximal cross-section A of H ✕ W = 3 ✕ 2 = 6 is between offsets 1 and 3. Note there's another one of area 6 for range [1..4], so the maximum is not necessarily unique.

The solution approach which seems to work is the following:

-
Create index variables left (L) and right (R) initially positioned at the extreme
left (0) and right (|hs|-1) of array hs.

-
Calculate the area as A = H ✕ W where H = min(hs[L], hs[R]) and W = R - L and record
it as the maximal area so far.

-
Move the lesser of L or R toward the other.

-
Repeat until R == L, then return the maximum recorded.

Code would look something

I would suggest the following $O(n)$ approach using a monotone stack which is nothing but a regular stack but also satisifes the invariant that its elements are in monotone order. Say you want to make a strictly monotone stack $S$ which is increasing viewed from the last in to the first out: you would process elements $x$ in order with the following policy: pop $S$ until it is empty, or until the top is $>x$, then push $x$.

Why might such a structure appear? Let's consider the half-problem where we find the largest container whose right side is smaller. (every container has a small side, which is why this is half a solution). Suppose that when viewed from left to right, we have 2 segments $h[i_1]$ and $h[i_2]$ with height $5$. Then clearly any container whose right and small side ends at $i_1$, can be extended to end at $i_2$, and the resulting container is strictly larger. Even further, we see that $i_1$ is made irrelevant by any $i_2>i_1$ and $h[i_2]\geq h[i_1]$. This "being made irrelevant" corresponds to the popping while building the stack, which can be implemented exactly as described above.

So now let's say we went through $i=1$ to $i=n$, and we have our stack. How do we actually calculate the largest containers with segments as the smaller right ends?

Again we go through $i=1$ to $i=n$, but with our stack in hand. Consider $h[1]$. Case 1) it is smaller than the top of the stack (call it $j$) then we can ignore it and move on, since the container formed with left side $h[1]$ and right side $h[j]$ is by definition not the type of container we are considering (we are only looking at right-side-smaller containers). And we can even ignore all containers with left side $h[1]$ and right side $h[j']$ for $j'$ under $j$ in the stack (because it is monotone). Case 2) if $h[1]\geq h[j]$, then $1$ is the best possible left side for a container whose right small side is $h[j]$. Ditto with any $j'$ under $j$ in the stack, which satisfies $h[1]\geq h[j]$. So we pop from the stack until we have some $h[1]< h[j]$, calculating the area each time, then continue with $i=2$, etc. It's not hard to prove that the stack empties, and that each time you pop an element from the stack, you have calculated the largest container with that element as its smaller right side.

StackExchange Computer Science Q#121472, answer score: 2