I read the paper multiple times, and I think I now understand everything up to Section 2.2.
What still confuses me is a logical gap from section 2.1 to 2.2. Section 2.1 discusses rules that validators must obey, and proves that, if the validators obey these rules, there is always a way for a validator to add a supermajority link to create new justified checkpoints.
Therefore, section 2.1 does not seem to prescribe any strategy for the validator on how to actually to create these links that lead to justified checkpoints.
Section 2.2 discusses the fork choice rule under assumption of existence of the longest justified checkpoint.
What seems to be missing is a description of a simple reasonable strategy that a validator should take.
It may be that a strategy as simple as “steps back in time” will work - namely that if a validator thinks that a particular checkpoint should be justified, it should first try to justify it using the shortest possible smartmajority link, and then if the attempt deadlocks due to a split vote, make other attempts for the same checkpoint moving the origin of the supermajority link back in history. I think there was a discussion that in case of a network split the situation can be remedied moving the origin of the supermajority link back in time to a point before the split.
I have a feeling that things will work well, and simple reasonable “keep trying” strategies can work in this case. What would be nice though is to fill what seems to be a gap in the paper by providing at least a brief discussion of these strategies.