上一章把问题化成估计 $\sum_h\mathrm{fourierTerm}(h)$。这一章处理其中「频率接近整数」的那一小撮项（主弧）。我们对 $\log\varphi_\theta$ 做带余项的二阶 Taylor 展开——这是全书唯一真正「算 Taylor 余项」的地方，我们一个常数都不含糊。线性项被上一章的质量恒等式消掉，二次项攒成一个高斯，最后得到一个显式的正下界 $\ge c_3/\sigma_E$。
先立记号。对实数 $x$，记 $\|x\|$ 为它到最近整数的距离（例如 $\|3.2\|=0.2$，$\|3.8\|=0.2$，$\|3.5\|=0.5$），总有 $0\le\|x\|\le\tfrac12$。「$h/e$ 接近整数」就是 $\|h/e\|$ 很小。
这个 $h\leftrightarrow m$ 的双射本身是纯组合的 CRT 记账，属于构造那一章的活；本章把它当已知，专心做分析——也就是把 $\mathrm{term\_label}(m)$ 这些项加起来。
要把 $\hat\mu(m)=\prod_e\varphi_{\theta_e}(m/e)$ 的连乘变成能求和的东西，标准动作是取对数把乘积变求和。所以先精确展开单个因子的对数。记 $t=m/e$（在主弧上 $|t|\le\tfrac1{10}$）。
证明——先定出精确的一、二次系数。把 $e(t)=e^{2\pi it}$ 按幂级数展开：
$$e(t)=\sum_{k\ge0}\frac{(2\pi i t)^k}{k!}=1+2\pi it-2\pi^2t^2-\tfrac{4}{3}\pi^3 i\,t^3+\cdots$$于是 $u:=e(t)-1=2\pi it-2\pi^2t^2+u_3$，其中 $u_3=\sum_{k\ge3}\dfrac{(2\pi it)^k}{k!}$ 是三次及以上的尾巴。特征函数写成 $\varphi_\theta(t)=(1-\theta)+\theta e(t)=1+\theta u$。令 $z:=\theta u$，用 $\log(1+z)=z-\tfrac{z^2}{2}+\tfrac{z^3}{3}-\cdots$：
$$\log\varphi_\theta(t)=z-\frac{z^2}{2}+\Big(\underbrace{\tfrac{z^3}3-\tfrac{z^4}4+\cdots}_{=:A}\Big).$$现在只保留到 $t^2$。$z=\theta u=2\pi i\theta t-2\pi^2\theta t^2+\theta u_3$；而 $z^2=\theta^2u^2$，其 $t^2$ 项来自 $(2\pi it)^2=-4\pi^2t^2$，故 $-\tfrac{z^2}2=2\pi^2\theta^2t^2+(\text{三次及以上})$。把一、二次项对齐：
这正是引理里的主部。剩下的全是三次及以上，收进 $R$。
把 $R$ 拆成「对数的高阶尾 $A$」与「$u$ 的三次尾造成的偏差 $B$」两块，逐块估：
（甲）对数尾 $A=\log(1+z)-z+\tfrac{z^2}2$。由 $|z|=|\theta u|\le|u|=|e(t)-1|=2|\sin\pi t|\le2\pi|t|$，当 $|t|\le\tfrac1{10}$ 时 $|z|\le\tfrac{2\pi}{10}\approx0.628<1$。用几何级数裂项， $$\|A\|\le\sum_{k\ge3}\frac{|z|^k}{k}\le\frac13\sum_{k\ge3}|z|^k=\frac{|z|^3}{3(1-|z|)}\le\frac{(2\pi)^3}{3\,(1-0.628)}\,|t|^3\approx222\,|t|^3.$$
（乙）三次尾偏差 $B$。直接代数化简（把已对齐的一、二次项减掉）得到闭式 $$B=\theta\,u_3-\frac{\theta^2}{2}\big(u^2-(2\pi it)^2\big).$$ 两块都显然是 $O(t^3)$：$|u_3|\le\tfrac{(2\pi|t|)^3}{6}e^{2\pi|t|}\le78|t|^3$；而 $u^2-(2\pi it)^2=(u-2\pi it)(u+2\pi it)$，其中 $|u-2\pi it|\le2\pi^2t^2+|u_3|\le28t^2$、$|u+2\pi it|\le4\pi|t|$，故第二块 $\le\tfrac12\cdot28\cdot4\pi\,|t|^3\approx176|t|^3$。合计 $\|B\|\lesssim250|t|^3$。
于是 $\|R\|\le\|A\|+\|B\|\lesssim 472\,|t|^3<10^3|t|^3$。Lean 里出于形式化便利用了更宽松的证书 $10^5|t|^3$（对数尾记成 $99000|t|^3$、二次匹配记成 $1000|t|^3$）——当然也成立，且宽松的常数在后面完全够用。本讲义用哪个都行，取 $10^5$ 与源码一致。$\qquad\blacksquare$
把引理 2.1 对每条边 $e$（取 $t=m/e$）相加。因为 $\log\hat\mu(m)=\sum_e\log\varphi_{\theta_e}(m/e)$：
$$\log\hat\mu(m)=2\pi i\,m\sum_{e}\frac{\theta_e}{e}\ -\ 2\pi^2m^2\sum_e\frac{\theta_e(1-\theta_e)}{e^2}\ +\ \delta_m,\qquad \delta_m:=\sum_e R(\theta_e,m/e).$$逐项看这三块：
合起来：
现在做「奇迹」那一步。取指数还原 $\hat\mu(m)=e^{\log\hat\mu(m)}$，再乘上 $\mathrm{term\_label}$ 里的 $e(-m/b)$：
$$\mathrm{term\_label}(m)=\hat\mu(m)\,e\!\Big(-\frac mb\Big) =\exp\!\Big(\underbrace{\tfrac{2\pi i m}{b}}_{=\,e(m/b)}-2\pi^2m^2\sigma_E^2+\delta_m\Big)\cdot e\!\Big(-\frac mb\Big).$$注意 $\exp(2\pi i m/b)=e(m/b)$，它与后面的 $e(-m/b)$ 精确相消！这就是把线性项收成「只依赖 $m$」的回报——相位被质量恒等式冲掉了。剩下：
$\exp(-2\pi^2m^2\sigma_E^2)$ 是一个正实数（高斯钟形）；$e^{\delta_m}$ 是模长接近 $1$ 的小复扰动。
证明。用不等式 $|e^{w}-1|\le e^{|w|}-1$（把 $e^w-1=\sum_{k\ge1}w^k/k!$ 逐项取模）。当 $|w|=\|\delta_m\|\le\tfrac1{10}$：
$$|e^{\delta_m}-1|\le e^{1/10}-1\approx0.1052.$$因此 $\mathrm{Re}\,e^{\delta_m}\ge 1-|e^{\delta_m}-1|\ge 1-0.1052=0.8948\ge0.8$。再乘上正的高斯因子即得。$\qquad\blacksquare$
把 §4 的逐项下界对 $|m|\le N$ 求和：
$$\mathrm{Re}\sum_{|m|\le N}\mathrm{term\_label}(m)\ \ge\ 0.8\sum_{|m|\le N}\exp\!\big(-2\pi^2\sigma_E^2 m^2\big).$$只剩最后一件事：给这个高斯和一个显式正下界。这纯粹是初等不等式，跟 $b$、跟边都无关。
证明——只保留中间几项，扔掉其余（都非负）。令 $M:=\big\lfloor\tfrac1{2\sigma}\big\rfloor$。只留 $m=0,1,\dots,M$ 这些项（它们都在窗口内，因为 $M\le\tfrac1{2\sigma}<\tfrac1\sigma\le N$）。对这些 $m$：
$$2\pi^2\sigma^2m^2\le 2\pi^2\sigma^2M^2\le 2\pi^2\sigma^2\Big(\frac1{2\sigma}\Big)^2=\frac{2\pi^2\sigma^2}{4\sigma^2}=\frac{\pi^2}{2},$$所以每一项 $\exp(-2\pi^2\sigma^2m^2)\ge e^{-\pi^2/2}$。这样的项共有 $M+1$ 个，而 $M+1=\lfloor\tfrac1{2\sigma}\rfloor+1\ge\tfrac1{2\sigma}$（因为 $\lfloor x\rfloor+1\ge x$）。既然被扔掉的项都非负，
$$\sum_{|m|\le N}e^{-2\pi^2\sigma^2m^2}\ \ge\ \sum_{m=0}^{M}e^{-2\pi^2\sigma^2m^2}\ \ge\ (M+1)\,e^{-\pi^2/2}\ \ge\ \frac1{2\sigma}\,e^{-\pi^2/2}=\frac{e^{-\pi^2/2}}{2\sigma}.\qquad\blacksquare$$主项其实是个纯实数——它的虚部精确为零。这来自一个漂亮的对称。
因此在对称窗口 $\{-N,\dots,N\}$ 上，$m$ 与 $-m$ 的项互为共轭，配对相加得 $2\,\mathrm{Re}\,\mathrm{term\_label}(m)$（实数），虚部两两抵消；$m=0$ 的项 $\mathrm{term\_label}(0)=\hat\mu(0)=\prod_e\varphi_{\theta_e}(0)=\prod_e 1=1$ 本身也是实的。所以
$$\mathrm{Im}\sum_{|m|\le N}\mathrm{term\_label}(m)=0,\qquad \sum_{|m|\le N}\mathrm{term\_label}(m)=\mathrm{Re}\sum_{|m|\le N}\mathrm{term\_label}(m).$$把 §4→§5 的实部下界与 §6 的虚部为零，经 §1 的双射 $S_M\leftrightarrow\{-N,\dots,N\}$ 搬回频率求和：
代入 $N\ge1/\sigma_E$ 用引理 2.3，再乘 §4 的因子 $0.8$：主弧实部 $\ge 0.8\cdot\dfrac{e^{-\pi^2/2}}{2\sigma_E}=\dfrac{c_3}{\sigma_E}$。数值上 $e^{-\pi^2/2}\approx e^{-4.93}\approx0.00720$，故 $c_3\approx0.8\times0.00360\approx2.9\times10^{-3}>0$——小，但确定为正，且随 $\sigma_E\to0$（即边越多越密）而放大。
下一章处理另一半：证明所有「远离整数」的频率贡献之和被压到这个峰之下。