Updating the blueprint

Stream: ABC-Exceptions

[Bhavik Mehta]

Now that the project is live, we should be sure that the blueprint accurately reflects the proofs we'd like people to work on. Am I correct that $S$ is not relevant any more, and we use only $N_\lambda$ and $S^*$? Could someone (maybe @Arend Mellendijk or @Jared Duker Lichtman) check this and update/remove def 1.5 and lemma 1.6 from the blueprint, accordingly?

[Bhavik Mehta]

In particular, it would be nice to clear up how to prove lemma 4.1, then I can do 4.4, and push the green blobs higher

[Arend Mellendijk]

$S$ is still mentioned in section 1 in reference to prior literature, which is why I didn't remove it when I rewrote section 2. Do we want to get rid of those comments too, or do we leave them in and remove the corresponding Lean declaration?

[Bhavik Mehta]

In my opinion the blueprint doesn't need that much motivation, since that's what the original paper is for. I think we should try to prove ABCTrivialBound, and TrivialBoundForSstar, but if S isn't necessary for those then my preference is to remove it from both the blueprint and Lean code

[Arend Mellendijk]

In particular, it would be nice to clear up how to prove lemma 4.1, then I can do 4.4, and push the green blobs higher

I think lemma 1.6 is still true for $S^*$, but the proof has some subtleties since we now have $\text{rad}(a) \le 2X^\alpha$ instead of $\text{rad}(a) \le X^\alpha$. That means we'd want De Bruijn's estimate stated as $\{n \le X : \text{rad}(n) \le 4x^\lambda \} \ll_\varepsilon x^{\lambda + \varepsilon}$. With that fix, Lemma 4.1 should be pretty immediate, right?

[Jared Duker Lichtman]

Don't worry about the trivial bound, just assume it as an axiom for now.

[Bhavik Mehta]

Perhaps, but it would be nice to be able to prove that too!