Extend and to hit at and , respectively. By easy angle chasing, , so is the midpoint of ; let denote the foot of the perpendicular from to (we want to show ). By Pascal's theorem on , there exists a point , so is cyclic. Thus
and similarly , as desired.

Alternatively, trig bash with POP to show that .

Interpret this as a graph , where all are good (i.e. belong to some triangle) and all are bad. We induct on to show that , where the base cases are vacuously true.

Now suppose . By Turán's theorem, we have a triangle . Suppose that .

If , then removing (and the edges incident to them) and noting that , the inductive hypothesis gives us at least
vertices in (the comes from ).

Otherwise, if , then by pigeonhole, WLOG
so is connected to some . Since , , so removing and applying the inductive hypothesis gives us
contradiction (the comes from ).

We want to find some monovariant . First, it's convenient to visualize the stacks as consecutive sets of lattice points in the first quadrant (e.g. lower left at ).

For simplicity, arrange the stacks in nonincreasing order (although it turns out this doesn't matter). Motivated by the final configuration, we take over all points corresponding to cards in our configuration. Suppose we have stacks of size , and is the smallest index such that . Then to compute , visualize the process as reflecting the points on over the line , shifting the points with via (up to this point, ), and then reordering the columns/stacks (here, , with equality iff ). Thus , with equality iff . (*)

There are finitely many configurations, so suppose we get into a loop with constant . Then we cannot have any of the nontrivial "reordering" mentioned in (*), i.e. in any step, we have if and if (so is preserved for each card). In particular, for fixed , the points with coordinates summing up to "cycle" along the line . Considering maximal , it's easy to see that because is a triangular number, this final loop must be a constant loop with and for , as desired.

Note that this method also determines the possible final states for not necessarily triangular.

Call a word good if it can be partitioned into two palindromes.

The possible operations are .

So there are basically two ways to look at the process: we can either think of it as directly showing and are good given , or we can think of it as "preserving" goodness through , etc. (basically stupid, forward induction vs. "reverse" induction).

The first way gets too messy quickly, so we focus on the more natural second way, i.e. by induction, it suffices to show that goodness is preserved by any of the substitutions , , , and .

Hence we consider what does to a palindrome (the other cases are analogous); it's easy to show (by comparing the left-to-right and right-to-left orientations) that if , then and (sorry for terrible notation) are palindromes.

Therefore if and for palindromes , then
as desired.

After playing around with this setup a bit (with contradiction), we see that the most annoying issue is "betweenness," which screws up a lot of positioning by forcing a lot of cases on us.

So we prove the projective dual instead, since lines are generally much more flexible with positioning: for a finite set of lines in the projective plane (not all concurrent), each colored red or blue, we prove that there exists a monochromatic point belonging to at least two lines of .

Indeed, suppose the contrary (WLOG, we work in the Euclidean plane by taking a suitable projection to ensure that no two lines intersect at infinity). Clearly, the blue lines are not all concurrent (same for the red lines).

Consider two lines of the same color passing through point . Then there exists a line of the other color passing through as well. Since not all lines of color pass through , there exists a line of color passing through a point . Let and .

The rest is easy: taking such a configuration with minimal area , must be monochromatic (color ), or else there exists a line through of color , and we get a smaller configuration (the line must intersect either segment or segment ).