User:Alemagno12/Six Trials of Formal Analysis

I've been a googologist/apeirologist for 9 years now, and have made many analyses ever since. However, all of my analyses have been heuristic guesses and analysis tables; I've since learned how to do formal proofs and I've tried to make formal analyses a few times now, but I've always lost motivation pretty quickly, leaving only a draft or an unfinished proof somewhere in the Googology Discord (see e.g this or this).

So I'm proposing myself six analysis challenges to become more familiar with formal analyses, which will hopefully motivate me to do more of them in the future:

1. HPrSS v1 by Yukito vs HPrSS v3 by Yukito (expected correspondence: lim(HPrSSv1) = HPrSSv3(0,3,5,2,5,7,4,7,9,5), from a 2018 heuristic analysis)
2. HPrSS v2 by Yukito vs HPrSS v3 by Yukito (expected correspondence: lim(HPrSSv2) = HPrSSv3(0,3,5,8,10,4), from a 2018 heuristic analysis)
3. [TBA] vs [TBA]
4. [TBA] vs [TBA]
5. Dropping Hydra (x = 1) by Hyp cos vs BM2.3 by Bashicu and koteitan (expected correspondence: lim(Dropping Hydra) = BM2.3(0,0,0)(1,1,1)(2,2,0))
6. Dropping Hydra (full) by Hyp cos vs BM2.3 by Bashicu and koteitan (expected correspondence: lim(Dropping Hydra(x+1)) = BM2.3(0,0,0)(1,1,1)(2,2,1)^x(2,2,0))