形式化证明的信任边界只有两处需要人肉核对：(a) Lean 定理是否表达了原问题；(b) 它依赖哪些公理、这些公理是否忠实转写自文献。本页把 Tang 证明的全部外部输入摊开来，逐条给出 Lean 原文与 Rosser–Schoenfeld 1962 出处。
axiom 声明（都在 RSPrimeSums.lean），外加 Lean 标准三公理 propext、Classical.choice、Quot.sound；0 个可达 sorry。因此 #print axioms erdos_306 精确输出 5 条公理、无 sorry。
两条公理都是把 J. B. Rosser 与 L. Schoenfeld 1962 年的经典结果原样写进 Lean。出处：Approximate formulas for some functions of prime numbers, Illinois J. Math. 6(1) (1962), 64–94，DOI 10.1215/ijm/1255631807。
RS Corollary 3, 式 (3.8), p. 69。对 $x\ge 20\tfrac12$，区间 $(x,2x]$ 中的素数个数满足 $$\pi(2x)-\pi(x)\ >\ \frac{3x}{5\log x}.$$ 这是 dyadic 区间里素数密度的下界（PNT 级别）。
axiom rosser_schoenfeld_cor3 (x : ℝ) (hx : (41 : ℝ) / 2 ≤ x) :
3 * x / (5 * Real.log x) <
(Nat.primeCounting ⌊2 * x⌋₊ : ℝ) - (Nat.primeCounting ⌊x⌋₊ : ℝ)RSPrimeSums.lean:41 · $\pi=$ Nat.primeCounting，$\lfloor\cdot\rfloor$ 为向下取整。
RS Theorem 5, 式 (3.17)/(3.18), p. 70。存在 Mertens 常数 $B$（RS 式 (2.10)，$B=0.26149721284764\ldots$），使 $$\log\log x+B-\frac{1}{2\log^2 x}<\sum_{p\le x}\frac1p\quad(x>1),\qquad \sum_{p\le x}\frac1p<\log\log x+B+\frac{1}{2\log^2 x}\quad(x\ge286).$$ 常数 $B$ 以存在量词给出（不钉死小数），正是 Theorem 5 的原样。历史源头：Mertens 1874。
axiom rosser_schoenfeld_thm5 :
∃ B : ℝ, ∀ x : ℝ,
(1 < x →
Real.log (Real.log x) + B - 1 / (2 * (Real.log x) ^ 2)
< ∑ p ∈ (Finset.Icc 2 ⌊x⌋₊).filter Nat.Prime, (1 : ℝ) / (p : ℝ)) ∧
(286 ≤ x →
∑ p ∈ (Finset.Icc 2 ⌊x⌋₊).filter Nat.Prime, (1 : ℝ) / (p : ℝ)
< Real.log (Real.log x) + B + 1 / (2 * (Real.log x) ^ 2))RSPrimeSums.lean:59 · 求和号即 $\sum_{p\le x}1/p$。
作者早期快照里曾把三条“dyadic 特化”当作局部公理；本快照已经全部降级为定理——这也解释了 README（说 2 条公理）与 Erdos306Final.lean 旧注释（说 3 条）的表面矛盾：README 正确，那条注释过时了。
| 项目事实 | 状态 | 来源 |
|---|---|---|
dyadic_prime_density每块素数个数 $\ge \dfrac{2^k}{2\log 2^k}$（$k\ge5$） | 定理 | 由公理一（Cor 3）推出：块基数 $=\pi(2^{k+1})-\pi(2^k)$，端点为合数、代入 $x=2^k$、把 $3/5$ 弱化到 $1/2$。RSPrimeSums.lean:118 |
dyadic_mertens_cumulative大 $k_0$ 时 $\sum_{p\in[2^{k_0},2^{3k_0+1})}1/p\ge \tfrac{21}{20}$ | 定理 | 由公理二（Thm 5）推出：块和 telescope 成 $S(2^{3k_0+1})-S(2^{k_0})$，常数 $B$ 抵消，$\log\log$ 差 $\ge\log 3>1.06$，误差项 $<0.003$。（真值极限 $\log 3\approx1.0986$。）RSPrimeSums.lean:234 |
dyadic_control_recipLoad_eventually_small控制边负载可任意小 | 定理 · 无数论公理 | 纯初等：控制边负载被 $\sum 1/k^2$ 尾部界住（$\le 512/(k_0-1)$），再取 $k_0$ 足够大。不用任何 RS 公理。R2BaseLoadUpper.lean:230 |
BlockSystem 的 hdensity 字段，支撑块系统 / CRT 能量机器（BlockSystemConstruction.lean:43、R2TopAssembly.lean:87）。BlockMassPool.lean:144）。这是质量批次必须超过的负载。axiom 声明grep -rn "axiom" *.lean 的真声明只有两条（其余是注释里的“axiom”一词）：
| file:line | 标识符 |
|---|---|
RSPrimeSums.lean:41 | rosser_schoenfeld_cor3 |
RSPrimeSums.lean:59 | rosser_schoenfeld_thm5 |
sorry严格 grep 只命中一处，且不可达：
| file:line | 可达？ |
|---|---|
GlobalControl.lean:778 | 否 —— 位于块注释 /- … -/ 内（第 766 行开，790 行闭）。这是被划掉的、原先错误的 mismatch_penalty 旧陈述；真正的 mismatch_penalty 在第 792 行、已证。 |
其它所有含“sorry”字样都是 docstring 散文（“fully proved, no sorry”“was a sorry”之类）。若干过时的 docstring（SBEEDispersion.lean:267、SBEEForcing.lean:780、GlobalControlG7.lean:120 等）写着“Status: sorry”，但其后引理体经逐文件 grep 确认不含任何 sorry/admit/sorryAx。
另外确认全树不含其它逃逸手段：admit、sorryAx、native_decide、Lean.ofReduceBool、@[implemented_by]、unsafe。
lake env lean RequestProject/Audit.lean 会打印：#check @erdos_306（陈述）、#print axioms erdos_306（依赖）、以及两条公理原文。CI 每次 push 重跑并 gate（若 erdos_306 可达任何 sorry 或超出许可公理集，构建失败）。
手工追踪的预期输出：
'erdos_306' depends on axioms:
[propext, Classical.choice, Quot.sound,
RosserSchoenfeld.rosser_schoenfeld_cor3,
RosserSchoenfeld.rosser_schoenfeld_thm5]即 Lean 标准三公理 + 两条 RS 公理 = 5，sorry-free。
cor3, thm5$\}$。