R2 构造与质量恒等式

1. 引擎的合同：`ArcConstruction`

引擎 exists_pos_weighted_of_construction（CircleMethodAssembly.lean:72）吃一个抽象记录 ArcConstruction T b，吐出 $0<\mathrm{Wcount}(E,\theta,b)$；正性再转成 Egyptian 表示 $\sum_{e\in S}1/e=1/b$，$S\subseteq E$ 全是避开障碍集 $T$ 的 squarefree 半素数。底层的唯一任务就是造出这个记录。

合同共 26 个字段（CircleMethodAssembly.lean:113）。按语义分四组：

组	字段	含义
边与权重	`E, theta, hsemi, havoid, hne, hlb, hub`	$E$ 是半素数边集，避开 $T$，非空；权重 $\theta_e\in[1/3,2/3]$。
周期与整除	`L, hL, hbL, heL, he0, hbound`	公共周期 $L$，$b\mid L$，每个 $e\mid L$，且整数和 $\sum_e\lfloor L/e\rfloor<L$。
质量核心	`hmass`	$\displaystyle\sum_{e\in E}\frac{\theta_e}{e}=\frac1b$ —— 整台机器的支点。
频率分区	`N, SM, Sm, lbl, hN, htw, hsmall, hpart, hdisj, hmaps, hinj, hsurj, hterm, hminor, Bm, hbeat`	把 $\{0,\dots,L-1\}$ 拆成主频 $S_M$（与 $[-N,N]$ 双射）和次频 $S_m$；主项 $\ge c_3/\sigma_E$，次项 $\le B_m$，且 $B_m<c_3/\sigma_E$（`hbeat`）。

两个关键量

$\sigma_E=\sqrt{\mathrm{sigmaE2}(E,\theta)}$，其中 $\mathrm{sigmaE2}=\sum_e\dfrac{\theta_e(1-\theta_e)}{e^2}$（方差尺度，CircleMethodMainTerm.lean:21）。
$c_3=0.8\cdot\dfrac{e^{-\pi^2/2}}{2}$（主项常数，r2MinorMainCtrlConstant）。hbeat 就是 $B_m<c_3/\sigma_E$，主项压过次项，逼出 $\mathrm{Wcount}>0$。

2. dyadic 块系统 `BlockSystem`

一切边都由素数积拼成，素数来自 dyadic 窗口里的“块”。BlockSystem（GlobalControl.lean:87）给出尺度 $k\in[k_0,K]$ 上的素数块 $P_k\subseteq[2^k,2^{k+1})$，密度近乎最大：

structure BlockSystem where
  k0 K : ℕ ;  hk : k0 ≤ K ;  hk0 : 1 ≤ k0
  P : ℕ → Finset ℕ
  hprime  : ∀ k, ∀ p ∈ P k, Nat.Prime p
  hwindow : ∀ k, ∀ p ∈ P k, 2^k ≤ p ∧ p < 2^(k+1)
  hdensity: ∀ k, k0 ≤ k → k ≤ K →
    (2^k : ℝ)/(2*Real.log (2^k)) ≤ (P k).card

密度字段 hdensity 的来源 RS 公理一

hdensity 就是定理 dyadic_prime_density（RSPrimeSums.lean:118），由 Rosser–Schoenfeld Corollary 3（$\pi(2x)-\pi(x)>3x/(5\log x)$）推出，把常数 $3/5$ 弱化到 $1/2$。见公理页。

存在性 exists_blockSystem（BlockSystemConstruction.lean:25）取 $k_0=\max(k_{0\min},5)$、$K=3k_0$、$P=\text{dyadicBlock}$（窗口内全体素数）。关键约束 admissibleGlobalRange（:212）：$2k_0\le K\le 3k_0$ —— 尺度数只随 $k_0$ 线性增长，这样支柱二 Peierls 论证里的因子 $\exp(A\cdot\#\text{blocks})$ 才受控。

3. 四族边

边集 $E=\text{ctrlEdges}\cup Q\cup\text{gadgetEdges}$（R2AssemblySkeleton.lean:72），拆成四个功能族：

图 · 四族边。控制边（蓝）给次弧机器提供块结构、负载压到很小；质量批次 Q（黄）贪心填满负载窗口以对上质量恒等式；gadget 边（紫）提供 multi-gadget 阻尼。全部是块素数或 $b$ 的素因子之积。

族	定义	素数来源	作用
E_int 块内	`internalPairs` 完全图 $p\cdot q$	同一块 $P_k$ 内	控制边，喂 CRT 能量机器
E_skel 骨架	`bipartitePairs` $P_k\times P_{k+1}$	相邻块	控制边，跨尺度连通
E_mass 质量批次 `Q`	贪心选的块素数积	`blockPrimes` 池	调质量、对上 $1/b$
E_gad gadget	`(R×S)` 映 $r\cdot s$	$r\in b$ 的素因子，$s\in P_{2k_0}$	次弧 multi-gadget 阻尼

避障：每条边 $\ge 2^{2k_0}>\sup T$（R2TopAssembly.lean:845），故 havoid 自动成立。

4. 均匀权重与质量恒等式

权重取均匀（R2Weights.lean:23）： $$\theta_e=\frac{1/b}{\mathrm{recipLoad}(E)}\quad(\forall e),\qquad \mathrm{recipLoad}(E)=\sum_{e\in E}\frac1e.$$ 于是质量恒等式变成一行代数（uniformTheta_mass，:68）： $$\sum_{e\in E}\frac{\theta_e}{e}=\theta\cdot\mathrm{recipLoad}(E)=\frac1b.\;\;\checkmark\ \text{(=\;hmass)}$$

调质量 = 命中一个负载窗口

因为 $\theta=\dfrac{1}{b\cdot\mathrm{recipLoad}(E)}$，所以

$$\theta\in[\tfrac13,\tfrac23]\iff \mathrm{recipLoad}(E)\in\Big[\tfrac{3}{2b},\tfrac{3}{b}\Big).$$

（uniformTheta_lower/upper_of_window，R2Weights.lean:33,50。）问题归结为：让全体边的倒数和落进 $[3/2b,\,3/b)$。

分两步命中窗口，$\mathrm{recipLoad}(E)=\text{baseLoad}+\mathrm{recipLoad}(Q)$（:132）：

① 底座压低无 RS 公理

baseLoad=recipLoad(ctrlEdges∪gadgetEdges) 保持 $<3/(2b)$（控制负载 $\le 3/(4b)$）。靠 dyadic_control_recipLoad_eventually_small（R2BaseLoadUpper.lean:230）：控制负载被 $\sum 1/k^2$ 尾部界住（$\le 512/(k_0-1)$），取 $k_0$ 够大即可。纯初等，不用任何数论公理。

② 质量批次填残差 RS 公理二

质量池的可用负载 $\ge 1/2$：用两个不同块素数之积 $pq$，其负载 $=(S^2-S_2)/2$，其中 $S=\sum_{p}1/p\ge 21/20$（Mertens 累积 dyadic_mertens_cumulative ⇐ RS Thm 5），得 $\approx0.535\ge1/2$（blockPrimes_product_load_ge_of，BlockMassPool.lean:144）。既然池够大而目标窗宽 $3/2b$，贪心 exists_residual_subset_recip_window（R2ConcreteData.lean:151）能选出 $Q$ 把 $\mathrm{recipLoad}(E)$ 精确落进 $[3/2b,3/b)$。

副产品：$\mathrm{recipLoad}(E)<3/b\le1$ 直接给出 hbound（$\sum_e\lfloor L/e\rfloor<L$，R2NumericFields.lean:72）。周期 $L=b\cdot\prod_{p\in\text{support}}p$（primeSupportPeriod），保证 $b\mid L$、每 $e\mid L$。

5. `exists_arcConstruction_final` 的装配顺序

theorem exists_arcConstruction_final (T : Finset ℕ) (b : ℕ)
    (hb : 3 ≤ b) (hbsf : Squarefree b) :
    Nonempty (ArcConstruction T b)

（R2TopAssembly.lean:756。$b=1,2$ 在 Erdos306Final.lean 用 $1=\tfrac12+\tfrac13+\tfrac16$、$\tfrac12=\tfrac13+\tfrac16$ 初等处理。）

量词顺序是承重的——先定常数、再据此定底层尺度 $k_0$：

常数层：$c_3$、$\eta=c_3/(2004b)$、从 multi-gadget lane 取 $C_{\text{tail}}$、$C=\max(C_0,3)\ge3$、$D_{mp}=c_3/(2004b(2C+3))$、gadget 个数 $G$（要 $\text{base}_b^{G}\le D_{mp}$，$\text{base}_b=\sqrt{1-(8/9)/b^2}$）。
底层：exists_r2_foundation_dyadic（:792）在满足所有阈值之和的底尺度 $k_0$（含 $k_0\ge10^6(\lceil C\rceil+1)^4$）造出块系统。
选边：gadget 素数 $S\subseteq\text{dyadicBlock}(2k_0)$（:804）；质量批次 $Q$ 经 r2_getQ（:808）。
权重：weights_of_recipLoad_window 给均匀 $\theta$ 与 hmass。
数值字段：$\sigma=\text{sigmaCtrl}(BS)$、$N=\lceil C/\sigma\rceil$；r2_close_numericFields（:1025）给 hN/htw/hsmall。$\sigma_E$ 夹逼 $\sqrt{2/9}\,\sigma\le\sqrt{\mathrm{sigmaE2}}\le501\,\sigma$。
次弧预算：$B_m=\big(b\eta+bC_{\text{tail}}e^{-C^2(16/9)/2}\big)/\sigma+b(2N+1)D_{mp}$，经 r2_close_budget_501 收成 hbeat。（次弧内部见支柱二详解。）
打包：exists_arcConstruction_of_mainArcParams（R2FinalAssembly.lean:137）建主弧双射（MainArcFields，$S_m:=\text{range }L\setminus S_M$）并封成 ArcConstruction。

6. 全链一览

exists_r2_foundation_dyadic  (BS, R=b.primeFactors)
  └ dyadic_prime_density        ⇐ RS Cor.3  【公理一】
exists_block_primes (S) ; r2_getQ (质量批次 Q)
  └ blockPrimes_product_load_ge ⇐ Mertens   【公理二】
  └ exists_residual_subset_recip_window  →  recipLoad(E)∈[3/2b,3/b)
weights_of_recipLoad_window   →  均匀 θ, hmass
r2_close_numericFields        →  hN, htw, hsmall
minor: G7 block lane + multi-gadget extra lane  →  hminor ; r2_close_budget_501 → hbeat
exists_arcConstruction_of_mainArcParams  →  打包
  → exists_arcConstruction_final
  → exists_pos_weighted_of_construction   (0 < Wcount)
  → erdos_306_unconditional

常数汇总：$c_3=0.8\cdot e^{-\pi^2/2}/2$；主项 $\ge c_3/\sigma_E$；Bernoulli 系数 $16/9$（$\theta=1/3$ 处 $8\theta(1-\theta)$）；$\theta\in[1/3,2/3]$；$\mathrm{recipLoad}(E)\in[3/2b,3/b)$；$\eta=c_3/(2004b)$；$C=\max(C_0,3)$，$N=\lceil C/\sigma\rceil$；$\text{base}_b=\sqrt{1-(8/9)/b^2}$；$\sqrt{2/9}\,\sigma\le\sigma_E\le501\sigma$；$k_0\ge10^6(\lceil C\rceil+1)^4$。