这是给学过一学期数学分析、但不是数学专业的读者写的。目标只有一个：把 Tang 的圆法证明里每一个数学细节都摊开，能自己一行行复算下来。凡是能讲清的，一步不省；凡是要引用现成结论的，明确告诉你引用了什么、为什么可信、以及它藏在 Lean 源码的哪一行。
站点上关于这个证明其实有三条平行的轨道，请按你的需要选：
| 轨道 | 给谁 | 公式量 |
|---|---|---|
| 人人能懂版 | 只想要直觉、一个公式都不想看 | 零 |
| 技术总览 + 4 详解页 | 已经懂圆法、只想快速核对结构与出处 | 密集，但只陈述引理不推导 |
| 本讲义（你在这里） | 学过数分、想把每步都弄明白 | 完整，每个界都从头算 |
七章基本是线性依赖的，建议顺序读。第一到第四章是「引擎」——一条从头到尾的主线，读完你就理解了「为什么这个证明能成立」。第五章讲怎么把引擎需要的原料造出来。第六章是全证里最硬的一环（能量-熵机制 + 一个漂亮的初等计数引理）。第七章交代整个证明唯一的两条外部公理。
每个公式后面若带一个灰色小标签（如 CircleMethod.lean:224），那是它在 Tang 的 Lean 源码里的确切位置，方便你或用户回去核对。你不需要会 Lean 也能读懂讲义——标签只是「可信度锚点」。
把这几样准备好，全程不会有第八样东西冒出来吓你：
你不需要：测度论 / Lebesgue 积分、复分析（留数、解析延拓）、解析数论背景（L-函数、筛法、Kloosterman 和）、概率论公理化。凡是名字唬人的（「圆法」「特征函数」「能量-熵」），我们都会就地用上面工具箱里的东西重新造出来。
是否每个有理数 $a/b$（$0<a/b$，且分母 $b$ 无平方因子）都能写成有限个互不相同的 $\dfrac1{pq}$ 之和，其中每个 $p\ne q$ 都是素数？（$pq$ 这种「两个不同素数之积」叫半素数，它天然无平方因子。）
答案是能。「分母 $b$ 必须无平方因子」这个限制的必要性是初等的（若 $b$ 含平方因子 $p^2$，任何 $\sum1/(p_iq_i)$ 通分后分母都不带 $p^2$，凑不出来）——这半边不难，本讲义不展开。真正硬的是充分性：给定合法的 $a/b$，怎么造出这样一组半素数。Tang 的证明解决的正是充分性。
整个证明先把问题层层削简（细节见第四章）：
于是所有难度集中到一件事：证明一个具体的和 $\mathrm{Wcount}$ 严格大于零。这就是「圆法」登场的地方。
下面这张图是整份讲义的地图。绿框是本讲义从头证到尾的部分；黄框是我们精确引用、不逐行展开的黑箱（第六章末与第七章会交代它们是什么、为什么可信）。箭头是「谁支撑谁」。
为了不骗你，我把话说在前面。这份讲义把整个证明的概念主干一步不省地推导出来；只有次弧最深处一坨机械记账（不是思想难，是页数多，完整展开约 150–260 页）我们给出精确陈述 + 证明策略 + Lean 定位，你或用户想看哪块，我随时展开。
| 内容 | 本讲义如何处理 | 在哪章 |
|---|---|---|
| Fourier 反演主恒等式 $L\cdot\mathrm{Wcount}=\sum_h\text{fourierTerm}$ | 完整推导（几何级数正交性起） | 一 |
| 主弧：Taylor 余项 → 高斯下界 $\ge c_3/\sigma_E$ | 完整推导（含 $10^5$ 常数来历） | 二 |
| 次弧初等半边：Jordan → 字符衰减 $16/9$ | 完整推导 | 三 |
| 拍频正性、抽取、顶层归约 | 完整推导 | 四 |
| 构造：质量恒等式、窗口调权、格张成 | 完整推导 | 五 |
| Lemma D（区间至多命中 2 点）+ 色散能量下界 | 完整推导（这是全证最漂亮的初等一步） | 六 |
| Peierls 能量-熵机制、G6 二分、G7 装配 | 完整推导逻辑 | 六 |
| Theorem B 覆盖二分 / G5 cold-master / Sector-I 地板 | 陈述 + 策略 + Lean 定位，按需展开 | 六 |
| 两条 Rosser–Schoenfeld 1962 数论事实 | 陈述 + 为何可信（唯一外部公理） | 七 |
把黄色两行以外的所有东西，你都能拿着这份讲义、一支笔、一学期数分的功底，独立复算出来。黄色两行不是「我们证不了」，而是「展开是机械劳动、篇幅巨大」——它们在 Lean 里已被 sorry-free 地证明，本讲义指到行号，随叫随展。