走到这里，全部数论「欠条」都能兑现了。整个 $\approx21{,}000$ 行的证明，除 Mathlib 外只引入两条命名公理——都是 1962 年 Rosser–Schoenfeld 的经典素数估计，且在 Lean 里逐字符照抄原始文献。前面各章遇到的所有数论黑箱（块内素数够多、块内倒数和 $\ge\tfrac{21}{20}$、控制载荷最终够小）都不是额外假设，而是从这两条推导出来的定理。这一薄章把它们精确列出、说明喂给谁、为何可信。
圆法引擎（第一~四章）、构造的调参与恒等式（第五章）、SBEE 的 Lemma D / 色散 / Peierls（第六章）——这些本讲义都零跳步证过，它们是纯分析与初等组合，不需要任何深的数论。真正需要「外部输入」的只有一件事：
「任意远处都存在一块素数，且这块素数的倒数和足够大」。第五章造边集时用它保证 (a) 素数取之不尽（避开集归纳）、(b) 块内倒数载荷够大以填进窗口 $[\tfrac3{2b},\tfrac3b]$。这是关于素数分布与倒数求和的定量事实，无法用初等代数变出来——它来自解析数论。
Tang 的做法很干净：不把「块内倒数和 $\ge\tfrac{21}{20}$」直接当公理，而是把两条教科书级的经典定理照抄进来当公理，再把实际用到的所有具体事实作为定理推导。这样公理面最小、且每条都能对着原始论文逐字核对。
Nat.primeCounting）。读法. 它说倍增区间 $[x,2x]$ 里的素数个数有一个正的下界 $\dfrac{3x}{5\log x}$。这正是「二进块 $[2^{k_0},2^{3k_0+1})$ 里素数管够」的来源——把 $x$ 取成 $2^{k}$ 逐段叠加，就得到块内足够多的素数（第五章 §2 的 dyadic_prime_density）。$x\ge20.5$ 的小门槛对我们要的大块毫无障碍。
读法. 它把素数倒数和 $\sum_{p\le x}1/p$ 两侧夹在 $\log\log x+B$ 附近，误差 $\le\dfrac1{2\log^2x}$。两式相减（在 $x$ 与 $2x$ 处）即得块内倒数和的下界——第五章 §2 的 $\sum_{p\in\text{block}}1/p\ge\tfrac{21}{20}$ 就是这么算出来的（dyadic_mertens_cumulative）。把 $B\approx0.2615$ 存在化（不钉死小数）让公理成为 Theorem 5 的精确转写。
两条公理都只在构造层被消费，喂出三条定理（不再是公理），再由它们支撑前面各章：
sorry-free 定理。axiom 声明连同门槛（$x\ge20.5$、$x\ge286$）、常数 $B$、eq. 编号都照抄原文，可对着 Illinois J. Math. 6(1) 第 69–70 页一字一句比对。本章只做「讲义视角」的说明。若要逐条核对整棵证明树对这两条公理的依赖、以及 #print axioms 级别的机器审计，请看内行向的 公理详解页（不在此重复其 ledger）。
七章合起来给出了 Erdős #306 一条自包含、逐行可复算的路径：
第一章 计数→圆 · 第二章 主弧高斯峰 · 第三章 次弧化能量 · 第四章 峰压谷→存在→主定理 · 第五章 造零件 · 第六章 能量胜熵 · 第七章 两条砖。
除本章两条经典公理外，每一步的积分、余项、常数都已摊开。$\blacksquare$