Let us formalize an appendix

Stream: PrimeNumberTheorem+

[Harald Helfgott]

Here is an appendix for which I would like to see a blueprint, and then a formalized version, in part because I would like to get the hang of the process, and in part because this is an explicit version of a basic, standard estimate. As you can see from the references I've left in, there are several versions in the literature, but this seems to be the first one in which the leading error term is optimal (in fact, it is no longer an error term: it is exact). It's part of a preprint I will soon put up on the arXiv.
PastedText.txt

[Harald Helfgott]

For everybody's convenience, let me extract the statements here.

Lemma A.1. Let $s = \sigma + i \tau$, $\sigma\geq 0$, $\tau\in \mathbb{R}$. Let $b>a>\frac{|\tau|}{2\pi}$; write $\rho = \frac{\tau}{2\pi a}$. Assume $a,b\in \mathbb{Z}+\frac{1}{2}$. Then, for any integer $n\geq 1$,

$$\begin{aligned}\int_a^b t^{-s} \cos 2\pi n t\, dt &= \left. \frac{(-1)^n t^{-s} \cdot \frac{\tau}{2\pi t}}{2\pi i \left(n^2 - \left(\frac{\tau}{2\pi t}\right)^2\right)}\right|_a^b \\ &+ \frac{a^{-\sigma-1}}{4\pi^2} O^*\left(\frac{\sigma}{(n-\rho)^2} + \frac{\sigma}{(n+\rho)^2} + \frac{|\rho|}{|n-\rho|^3} + \frac{|\rho|}{|n+\rho|^3}\right).\end{aligned}$$

[Harald Helfgott]

Proposition A.2 Let $s = \sigma + i \tau$, $\sigma\geq 0$, $\tau\in \mathbb{R}$. Let $a\in \mathbb{Z} + \frac{1}{2}$ with $a>\frac{|\tau|}{2\pi}$. Then

$$\zeta(s) = \sum_{n\leq a} \frac{1}{n^s} - \frac{a^{1-s}}{1-s} + c_\rho a^{-s} + O^*\left(\frac{C_{\sigma,\rho}}{a^{\sigma+1}}\right),$$

where $\rho = \frac{\tau}{2\pi a}$, $c_\rho = \frac{i}{2} \left(\frac{1}{\sin \pi \rho} - \frac{1}{\pi \rho}\right)$ and $C_{\sigma,\rho}= \frac{\sigma}{2} \left(\frac{1}{\sin^2\pi \rho} - \frac{1}{(\pi \rho)^2}\right) + \frac{|\rho|}{2\pi^2} \left(\frac{1}{(1-|\rho|)^3} + 2\zeta(3)-1\right)$.

[Harald Helfgott]

Let us use perhaps a letter other than $\rho$, since it may be best in this context to reserve $\rho$ for zeros of the $\zeta$ function.

[Harald Helfgott]

@Terence Tao told me the proofs in the text I posted were a bit long. I've now broken up what was Lemma A.1 (see above) as much as I could without sacrificing readability. I think this is essentially a blueprint, or as close to a blueprint as it can be without human-unfriendly - but it's my first attempt at such a thing (purpleprint?), so do give me feedback as to whether this is the right level of detail.

If people like this, I'll do much the same for the second half of the appendix, where Proposition A.2 in the above is proved.
appendixA1.pdf

You can ignore everything before section A.1, except for the notation line. I'm including the introduction to appendix A just for context.
PastedText.txt

[Terence Tao]

I'll start on converting this. Do you have the bibtex file for the references? I can just use placeholders for the time being.

EDIT: for future reference, it would be good to minimize use of custom macros such as \TV unless they are also included in the LaTeX provided; also any unusual LaTeX packages (e.g. dsfont) should either be avoided or included explicitly.

[Terence Tao]

The first half of the appendix is now blueprinted and issued: PNT#546 PNT#547 PNT#548 PNT#549 PNT#550 PNT#551 PNT#552 https://alexkontorovich.github.io/PrimeNumberTheoremAnd/blueprint/zeta-chapter.html#a0000000031. I am taking advantage of the project metadata to flag these formalization tasks as "small", "medium", or "large" based on my subjective impression of difficulty.

[Harald Helfgott]

Hi Terry,

Thanks! Here is the .bbl file.

I take this means I am doing the right thing - that is, what I've provided is tex/pdf files at the right level of detail to be converted very easily into a blueprint? If so, I'll go ahead and do the same for the second half of the Appendix.

Of course I could set up and upload the blueprint itself, if I knew how to. Is there a FAQ? In the meantime, I'll just continue working this way, since pdf files are easier to read, it doesn't seem to burden everyone overly, and it introduces another layer of feedback.

Also, can you add a reference to my upcoming preprint (or tell me how to add it), which is where this pdf is coming from? I don't want arXiv or a journal think I'm plagiarizing the project.

[Harald Helfgott]

PS. Where do I see the metadata, and your difficulty assessments more particularly?

[Terence Tao]

The .bbl file was not attached.

The level of granularity of the blueprint seems appropriate; I see that one of the components PNT#547 has already been claimed. If you expand the "PNT+ Project" window of the right of that page you will see the metadata, in particular a labeling of this task as "medium" in size.

Going forward it will probably be a useful skill for you to be able to obtain a local copy of the Github repository at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd and build the blueprint locally, although the precise mechanics for this is a bit complicated to explain (and is dependent on what type of OS you have and what Git interface you are using). But it is relatively easy to make pull requests to make small additions or edits to the files. For instance, to edit the bibliography, one can start from the Githut repo, click on "blueprint/src" and then "references.bib" to arrive at https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/main/blueprint/src/references.bib, then click on the edit button (a pencil icon on the top right) to propose an edit (you may need to first set up a Github account for this). You can make the edits and then press the "Commit changes" button, and that should lead to a pull request that I (or some other project maintainer) can later approve. Perhaps as a test edit you can upload the bibliography and make the reference to the forthcoming preprint as you suggest?

[Harald Helfgott]

Let me see. Here is the bbl file for now; I'll try uploading it as you suggest after I have dinner and finish preparing a talk for tomorrow.
sqappendixvar.bbl

[Harald Helfgott]

I have Linux. I am a Git novice - what Git interface do you recommend?

[Terence Tao]

I haven't used Linux in two decades (other than a few half-hearted experiments with WSL); perhaps someone more familiar with modern Linux distributions can make a suggestion. (On Windows, the Github extension on VSCode works nicely, especially since I was already using VSCode for my Lean, LaTeX and Python writing; I believe VSCode is also available on Linux, but may not be the best choice on that OS.)

[Alex Kontorovich]

Harald, do you use any LLMs? I also didn't know what Git was when I started working with Lean. These days, you can ask your favorite LLM and it will tell you how to customize your workflow to your liking...

[Harald Helfgott]

Sure, I use LLMs, but I prefer to ask an expert :).

[Snir Broshi]

(speaking as a random SWE)
I recommend using the integration in whatever editor you're using (e.g. VSCode's git panel, perhaps installing "GitLens" to see blame on the current line, and "Git Graph" to solve more complex situations).
If you want to go fancy you can use GitKraken.

[Harald Helfgott]

Here's a LaTeX near-blueprint (purpleprint?) for the rest of the appendix. I'm also including the PDF output for the entire appendix. Hope this is at the right level of detail. You can of course omit most of the explanatory passages in the actual blueprint.

[Harald Helfgott]

Actually, let me replace those by slightly more structured versions. Here they are.
PastedText.txt
appendixA.pdf

[Terence Tao]

These are now blueprinted and issued. PNT#566 PNT#567 PNT#568 PNT#569 PNT#570 PNT#571 PNT#572 PNT#573

[Harald Helfgott]

Thanks!

[Harald Helfgott]

Do feel free to tell me if, in the future, it would be better if things were more detailed, less detailed, etc., further split up, etc.

[Terence Tao]

@Pietro Monticone is reporting that many of the tasks in the appendix (which I have mostly tagged as "small" (roughly comparable to 1-3 line informal proofs with just one or two inputs) or "medium" (comparable to 3-6 line proofs with multiple inputs) are in fact within reach of autoformalization, so this is a pretty good level of granularity.

With Github Copilot, converting the LaTeX to the blueprint format, and spelling out the Lean formalization, has been actually rather straightforward; in several later cases, once a couple of the lemmas had been translated in this fashion to provide sufficient context, the rest could be handled almost entirely by Copilot's autocomplete. The main time-consuming issue has been with external LaTeX dependencies, such as macros not defined within the text, or references not supplied. So it would be good if you could check that any future LaTeX file you supply compiles on its own without the need for dependencies.

[Pietro Monticone]

Yes, exactly. I submitted a single request to Aristotle with PNT#546, PNT#547, PNT#548, PNT#549, PNT#550, PNT#551 and PNT#552 (i.e. all those available in the file at the time) and it solved all of them in one go apart from PNT#546 and PNT#550 for some reasons I'll explore tomorrow.

I've just submitted another request for the new PNT#566 to PNT#573.

Let's see.

[Harald Helfgott]

Nice! Tell me if things would be fine with less granularity (for the sake of human readers).

I'll be careful to submit full .tex files with their .bbl files in the future - sorry about that. Can you sketch the exact workflow, so that I can try my hand at doing these things myself in the future? What do I need to do to let Github Copilot (available on VSCode?) take care of converting LaTex to the blueprint format, however defined? And what do you mean by "spelling out the Lean formalization" - can Copilot actually take care of translating the blueprint statements (not their proofs) into Lean statements? (I need to learn more Lean before I can check myself that such translations are correct.) And how do I call Aristotle?

[Pietro Monticone]

Nice! Tell me if things would be fine with less granularity (for the sake of human readers).

This granularity should be fine, but I'll be able to give a more accurate response later today / tomorrow.

[Alex Kontorovich]

Pietro Monticone said:

Yes, exactly. I submitted a single request to Aristotle with PNT#546, PNT#547, PNT#548, PNT#549, PNT#550, PNT#551 and PNT#552 (i.e. all those available in the file at the time) and it solved all of them in one go apart from PNT#546 and PNT#550 for some reasons I'll explore tomorrow.

I've just submitted another request for the new PNT#566 to PNT#573.

Let's see.

How hard would it be to engineer Aristotle to automatically try an Issue every time it's posted...?

[Terence Tao]

What I have been doing is pasting in the tex file as a comment to the Lean file. Any commentary that isn't part of a theorem can be easily converted to a blueprint_comment field (see e.g., this example). Actually any theorem or lemma could also be placed in a blueprint_comment initially, which would already generate a bare-bones blueprint in which the lemmas are not yet linked to any Lean statement.

To start linking things up, I need to replace each theorem or lemma in the comments with Lean code of the form

@[blueprint
  "<label of theorem>"
 (title := "<title of theorem>") -- Optional
 (statement := /-- <statement of theorem> -/)
 (proof := /-- <proof of theorem> -/)
 (latexEnv := "<theorem type>")  -- e.g., "lemma", "sublemma", etc.  Default: "theorem".
 (discussion := <issue number on github>)] -- can be added later
theorem name_of_theorem <hypotheses> : <conclusion> := by sorry

Everything except the last line can be populated easily from the latex commentary, and in fact after doing this once or twice, Github Copilot "catches on" to what I am doing and can autocomplete all this. It also does a reasonable job autocompleting the Lean code itself, although it occasionally gets the syntax wrong and misses some subtleties e.g., with real vs complex exponentiation. Some of the style choices made by Copilot I disagreed with; for instance, in situations where some inline definitions are made in the theorem (e.g. "where $\varphi_\nu(t) = \nu t - \frac{\tau}{2\pi} \log t$"), Copilot would initially expand out these definitions (e.g., replacing each appearance of $\varphi_\nu(t)$ with $\nu t - \frac{\tau}{2\pi} \log t$), but the first few times it did this, I rewrote the theorem using let statements instead (e.g., let φ : ℝ → ℝ := fun t ↦ ν * t - (s.im / (2 * π)) * Real.log t) and then after that, Copilot copied my style. Similarly, Lean does not provide convenient support for the $O_*(X)$ notation, so I replaced statements such as $X = Y + O_*(Z)$ with ∃ E, X = Y + E ∧ ‖E‖ ≤ Z instead, and again Copilot figured out what I was doing after one or two such instances and autotranslated subsequent uses of the $O_*()$ notation largely to my satisfaction.

In some cases, some additional definitions need to be made that don't naturally fall into any of the formally blueprinted statements, and I just add them by hand; for instance, the notion of a half-integer came up at several points, so I just added a definition for this concept manually rather than create a formal blueprint definition for what a half-integer is.

If you like, I could record a video of myself doing this for a future LaTeX pre-blueprint to illustrate the process.

[Harald Helfgott]

@Terence Tao that would be fantastic.

For what it's worth: I've participated in a couple of Lean for the Curious Mathematician workshops, done the Numbers game, etc., besides having experience in a couple of programming languages (though what I program in regularly is C and Python, which are not so relevant, and the only conceptually clean language in which I have ever truly programmed is Scheme, which is in the antipodes of Lean in some respects). Taking a look now, I see I can figure out more or less what a Lean theorem statement says, but I wouldn't be able to tell with any confidence whether it's missing a subtlety, or even something that is not so subtle. (The closest comparison would be my experience as a native speaker of a Romance language who also knows some classical Greek: I can often figure out the general meaning of a Latin sentence, but I certainly would not say I know Latin, never having studied it.) I imagine I have to up my game for all of this? Any suggestions on how to go about it?

[Terence Tao]

The standard route (at least as of 2023, which is when I started learning Lean) is to work through a few chapters of Mathematics in Lean, in particular following the instructions at the beginning to clone the repository and start filling in some sorries locally on your own computer. Though there may be slightly more modern options now, perhaps some other participants on this channel can suggest some.

[Pietro Monticone]

I think more granularity would help.

[Harald Helfgott]

@Pietro Monticone It would be good to have an example of where a lack of granularity in the blueprint for my appendix might be a non-trivial obstacle for formalization. I'm a bit reluctant to split things up further just for safety, as things are getting a bit past the limit where I find them to be still natural as a human (self-)reader.

[Pietro Monticone]

Overall I think the current level is probably the best human-machine compromise. I'll share some examples later when they're ready

[Terence Tao]

In general I think it is best to think of the blueprint document as decoupled from a document intended to be read primarily by humans in the traditional fashion. So, rather than try to create a unitary document that is suitable both for blueprinting and for reading traditionally, one should generate two separate documents, one on the level of an arXiv preprint that can be read by humans, and the other which is aimed at either human or AI formalizers and requires a lot less motivation, citation of references, etc..

[Harald Helfgott]

I wonder how the blueprint or near-blueprint document gets archived (or arxived) then, though - isn't there a danger that it get lost in the heat of the battle? And do we really want a blueprint that is not readable in the traditional sense?

[Terence Tao]

To me the blueprint plays a role similar to code documentation: a living technical document that is not intended to be read in a linear fashion, but instead serving as a reference that one consults as needed in order to understand a given step in a larger argument. In particular, as with other reference materials such as dictionaries or Wikipedia, there is only a need for local rather than global narrative structure; as long as the blueprint can explain clearly how Lemma n follows from (say) Lemmas n-1, n-2, and n-3 for each value of n, it serves its purpose.

Github repositories maintain version control on all prior instances of these documents, so one can in principle roll back a blueprint to any given point in time if desired. It's a different model from a static arXiv preprint (though even the arXiv supports replacing one timestamped version of a preprint with another), but is an equally valid form of "publication" in my view.

[Yongxi Lin (Aaron)]

Is it possible to update Mathlib in the PNT repository? I am working on PNT#569 and I want to take advantage of the theorem EisensteinSeries.tendsto_zero_inv_linear, which I believe is not in the PNT repository right now.

[Pietro Monticone]

Yongxi Lin (Aaron) said:

EisensteinSeries.tendsto_zero_inv_linear

Doing it.

[Pietro Monticone]

Opened PNT#621 for tag release purposes and then I'm going to bump Mathlib once more to get EisensteinSeries.tendsto_zero_inv_linear

[Pietro Monticone]

Opened PNT#623 to bump mathlib to main.

[Pietro Monticone]

Aristotle disproved lemma_abadsumas with the counterexample (s=0, a=1/2, b=3/2).

theorem lemma_abadsumas {s : ℂ} (hs1 : s ≠ 1) (hsigma : 0 ≤ s.re) {a b : ℝ} (ha : 0 < a)
    (hab : a < b) (ha' : a.IsHalfInteger) (hb' : b.IsHalfInteger) (haτ : a > |s.im| / (2 * π)) :
    let ϑ : ℝ := s.im / (2 * π * a)
    let ϑ_minus : ℝ := s.im / (2 * π * b)
    let f : ℝ → ℂ := fun y ↦
      if a ≤ y ∧ y ≤ b then (y ^ (-s.re) : ℝ) * e (-(s.im / (2 * π)) * Real.log y) else 0
    let g : ℝ → ℂ := fun t ↦
      if t ≠ 0 then (1 / Complex.sin (π * t) : ℂ) - (1 / (π * t : ℂ)) else 0
    let C : ℝ :=
      if ϑ ≠ 0 then
        s.re / 2 * ((1 / (Complex.sin (π * ϑ) ^ 2 : ℂ)).re - (1 / ((π * ϑ) ^ 2 : ℂ)).re) +
          |ϑ| / (2 * π ^ 2) * ((1 / ((1 - |ϑ|) ^ 3 : ℝ)) + 2 * (riemannZeta 3).re - 1)
      else
        s.re / 6
    ∃ E : ℂ, ∑' n : ℤ, (Real.fourierIntegral f n + Real.fourierIntegral f (-n)) =
      ((a ^ (-s) : ℂ) * g ϑ) / (2 * I) - ((b ^ (-s) : ℂ) * g ϑ_minus) / (2 * I) + E ∧
      ‖E‖ ≤ C := by
  -- Wait, there's a mistake. We can actually prove the opposite.
  negate_state;
  -- Proof starts here:
  refine' ⟨ 0, _, _, 1 / 2, 3 / 2, _, _, _, _ ⟩ <;> norm_num [ Real.pi_pos.le ];
  · exact ⟨ 0, by norm_num ⟩;
  · refine' ⟨ ⟨ 1, _ ⟩, _ ⟩ <;> norm_num [ ZetaAppendix.e ];
    ...

@Terence Tao I'll open a PR soon to substitute (hsigma : 0 ≤ s.re) with (hsigma : 0 < s.re).

[Pietro Monticone]

Opened PNT#809.

[Harald Helfgott]

Aha - is this really a misformalization, as PNT#809, or is there something off with the statement in TeX/PDF?

[Harald Helfgott]

Hm, for s = 0, both side of the equation in the PDF are 0, so the result should be correct.

[Pietro Monticone]

Oh, wait, also the error bound is misformalised, right?

[Harald Helfgott]

Something must be misformalized - I'm not sure what. One should not have to require sigma>0; the lemma should also be correct for sigma=0.

[Pietro Monticone]

Yes, I think that we should just fix the error bound.

[Pietro Monticone]

So the formalised statement becomes:

theorem lemma_abadsumas {s : ℂ} (hs1 : s ≠ 1) (hsigma : 0 ≤ s.re) {a b : ℝ} (ha : 0 < a)
    (hab : a < b) (ha' : a.IsHalfInteger) (hb' : b.IsHalfInteger) (haτ : a > |s.im| / (2 * π)) :
    let ϑ : ℝ := s.im / (2 * π * a)
    let ϑ_minus : ℝ := s.im / (2 * π * b)
    let f : ℝ → ℂ := fun y ↦
      if a ≤ y ∧ y ≤ b then (y ^ (-s.re) : ℝ) * e (-(s.im / (2 * π)) * Real.log y) else 0
    let g : ℝ → ℂ := fun t ↦
      if t ≠ 0 then (1 / Complex.sin (π * t) : ℂ) - (1 / (π * t : ℂ)) else 0
    let C : ℝ :=
      if ϑ ≠ 0 then
        s.re / 2 * ((1 / (Complex.sin (π * ϑ) ^ 2 : ℂ)).re - (1 / ((π * ϑ) ^ 2 : ℂ)).re) +
          |ϑ| / (2 * π ^ 2) * ((1 / ((1 - |ϑ|) ^ 3 : ℝ)) + 2 * (riemannZeta 3).re - 1)
      else
        s.re / 6
    ∃ E : ℂ, ∑' n : ℤ, (FourierTransform.fourier f n + FourierTransform.fourier f (-n)) =
      ((a ^ (-s) : ℂ) * g ϑ) / (2 * I) - ((b ^ (-s) : ℂ) * g ϑ_minus) / (2 * I) + E ∧
      ‖E‖ ≤ C / a ^ (s.re + 1) := by
  sorry

[Pietro Monticone]

This way we don't need any strict inequality for hsigma.

[Harald Helfgott]

Right, but I'm not sure what the difference will be for s=0, since C will be 0 anyhow.

[Harald Helfgott]

Other than changing $C$ (incorrect) to $C / a ^ {s.re + 1}$, have you changed anything?

[Pietro Monticone]

No

[Harald Helfgott]

OK, try that, but something is odd here.

[Pietro Monticone]

We're also including $n = 0$ in ∑' n : ℤ, (FourierTransform.fourier f n + FourierTransform.fourier f (-n)).

It should be either:

∑' n : ℕ+, (FourierTransform.fourier f n + FourierTransform.fourier f (-n))

or

∑' n : ℕ, (FourierTransform.fourier f (n + 1) + FourierTransform.fourier f (-(n + 1 : ℤ)))

So I think the real bug exploited by Aristotle is just that the sum includes $n = 0$, but the LaTeX correctly intends $\sum_{n \geq 1}$.

[Pietro Monticone]

Ok, updated the PR PNT#809.

[Paul Nelson]

I'll try PNT#546 if that's still unclaimed

[Terence Tao]

Great! For the purpose of issue tracking, could you reply "claim" on that issue?

[Alex Nguyen]

In PNT#570, I'm slightly confused by a detail: the lean statement is written (π ^ 2 / (sin (π * z) ^ 2 : ℂ)) = ∑' (n : {m : ℤ // m > 0}), (1 / ((z - n) ^ 2 : ℂ)) but the blueprint formula is written $\frac{\pi^2}{\sin^2 \pi z} = \sum_{n=-\infty}^\infty \frac{1}{(z-n)^2}$. In the lean statement, the sum is over the positive integers but in the blueprint, the sum is over all integers. Is this intentional ? Apologies if I misunderstood something.

[Harald Helfgott]

This has to be a misformalization. Thanks for pointing it out.

[Terence Tao]

Yes, probably due to a previous issue where another sum was incorrectly stated to range over the integers but needed to only be over the positive integers, and the correction was mistakenly propagated to this lemma as well. Feel free to correct the statement if you want to claim it (this is part of what the formalization process is meant to do anyways).

[Alex Nguyen]

Thank you both. Just to clarify, this means that the blueprint formula is correct, and the lean statement should be (π ^ 2 / (sin (π * z) ^ 2 : ℂ)) = ∑' (n : ℤ), (1 / ((z - n) ^ 2 : ℂ)) ?

[Kevin Buzzard]

At least in this variant not one but both sides are invariant under z maps to z+1 :-)

[Kevin Buzzard]

What's the type of z by the way? If it's a complex number then it's hard to believe that all these coercions to C are needed

[Alex Kontorovich]

Yes, z : ℂ so those coercions are not necessary (probably added by copilot)...

[Alex Nguyen]

I'd like to check a potential misformalization: In PNT#568 the limit reads $\lim _{N \rightarrow \infty} \sum_{n=1}^N(\widehat{f}(n)+\widehat{f}(-n))$, but the lean code reads ∑ n ∈ Ioc 1 N, which is a sum $\lim _{N \rightarrow \infty} \sum_{n=2}^N$

[Terence Tao]

Oops, that was me overcompensating for including 0 in my summations too often. One can fix to Icc 1 N (or Ioc 0 N if you prefer).

[Alex Nguyen]

I'd like to check a potential sign error in PNT#573. As in the blueprint I managed to prove
$\sum_{n \leq a} \frac{1}{n^s}=\zeta(s)+\frac{a^{1-s}}{1-s}-\frac{a^{-s} g(\vartheta)}{2 i}+O^*\left(\frac{C_{\sigma, \vartheta}}{a^{\sigma+1}}\right)+\frac{b^{-s} g\left(\vartheta_{-}\right)}{2 i}+O^*\left(\frac{2|s|}{\sigma b^\sigma}\right)$
Given that $-\frac{g(\vartheta)}{2 i}=c_{\vartheta}$
Therefore, we have $\sum_{n \leq a} \frac{1}{n^s}=\zeta(s)+\frac{a^{1-s}}{1-s}+c_{\vartheta} a^{-s}+O^*\left(\frac{C_{\sigma, \vartheta}}{a^{\sigma+1}}\right)+\frac{b^{-s} g\left(\vartheta_{-}\right)}{2 i}+O^*\left(\frac{2|s|}{\sigma b^\sigma}\right)$
Rearranging to solve for $\zeta(s)$ and take $b \rightarrow \infty$, then we should instead have
$\zeta(s)=\sum_{n \leq a} \frac{1}{n^s}-\frac{a^{1-s}}{1-s}-c_{\vartheta}a^{-s}+O^*\left(\frac{-C_{\sigma, \vartheta}}{a^{\sigma+1}}\right)$
The blueprint and lean statement both have a $+ c_{\vartheta}a^{-s}$ term instead

[Terence Tao]

The blueprint and lean statement are derived from Proposition A.14 of Harald's appendix. Harald notes that this term has not previously been recorded in the literature, so it is possible that it was computed with a sign error. @Harald Helfgott , could you confirm? On my reading I agree with Alex that the sign on $c_\vartheta$ needs to change at the last line of the proof when writing everything in terms of $\zeta(s)$.

[Harald Helfgott]

I think you are quite right; $c_\vartheta$ should be defined as $\frac{i}{2} \left(\frac{1}{\pi \vartheta}- \frac{1}{\sin \pi \vartheta}\right)$ instead.

(Incidentally, I'm not seeing why there is an $O^*(2 |s|/(\sigma b^\sigma))$ here and not an $O^*(|s|/(2\sigma b^\sigma))$; of course $b\to \infty$, so in the end it doesn't matter, but I may have been silly.)

[Alex Nguyen]

Thank you ! What's your preferred way of fixing this -- should I define $c_{\vartheta}$ as $\frac{i}{2}\left(\frac{1}{\pi \vartheta}-\frac{1}{\sin \pi \vartheta}\right)$ or change $+c_{\vartheta} a^{-s}$ to $-c_{\vartheta} a^{-s}$ ? It looks like you're suggesting the former but I'd like to confirm.

[Harald Helfgott]

It really doesn't matter. Maybe the latter, so that $c_\vartheta$ will be positive imaginary when $\vartheta$ is positive?