1. Wcount：把概率写成计数
Wcount 定义 CircleMethod.lean:48
$$\mathrm{Wcount}(E,\theta,b)=\sum_{S\subseteq E}\mathbf 1\!\Big[\sum_{e\in S}\tfrac1e=\tfrac1b\Big]\ \Big(\prod_{e\in S}\theta_e\Big)\Big(\prod_{e\in E\setminus S}(1-\theta_e)\Big).$$
这是一个概率的确定性改写。给每条边 $e$ 一个独立 Bernoulli($\theta_e$) 指示 $\xi_e$；子集 $S$ 被选中的权重是 $\prod_{e\in S}\theta_e\prod_{e\notin S}(1-\theta_e)$。于是
$$\mathrm{Wcount}(E,\theta,b)=\mathbb P\Big(\sum_{e:\ \xi_e=1}\tfrac1e=\tfrac1b\Big),$$
且 $\mathrm{Wcount}>0$ 等价于存在这样的子集（反向见 §6）。关键洞察：把“存在性”问题转成“某个概率是否为正”，而概率可用 Fourier 反演逐频率估计。
Bernoulli 特征函数 BernoulliFourier.lean:27,33
$\varphi_\theta(t)=(1-\theta)+\theta e^{2\pi it}$，模方精确为
$$|\varphi_\theta(t)|^2=1-4\theta(1-\theta)\sin^2(\pi t).$$
这条恒等式是两条弧的种子：$t\approx0$ 时接近 1（主弧），远离整数时 $\sin^2$ 强迫衰减（次弧）。
2. Fourier 反演主恒等式
有限加性字符正交（CircleMethod.lean:98）：$\sum_{h<L}e(hn/L)=L\cdot\mathbf 1[L\mid n]$。在“无环绕”假设 $\sum_{e\in E}\lfloor L/e\rfloor<L$ 下，整除被桥接到精确倒数恒等式（fourier_indicator，:132）：
$$L\ \Big|\ \Big(\sum_{e\in S}\tfrac Le-\tfrac Lb\Big)\iff\sum_{e\in S}\tfrac1e=\tfrac1b.$$
组合正交 + 指示 + Bernoulli 乘积展开，得主恒等式（wcount_fourier_identity，:224）：
主恒等式
$$L\cdot\mathrm{Wcount}(E,\theta,b)=\sum_{h=0}^{L-1}\mathrm{fourierTerm}(h),\qquad
\mathrm{fourierTerm}(h)=\hat\mu(h)\,e(-h/b),\ \ \hat\mu(h)=\prod_{e\in E}\varphi_{\theta_e}(h/e).$$
即 $\mathbb P(Y=L/b)=\tfrac1L\sum_{h<L}\hat\mu(h)e(-h/b)$，$Y=\sum_e\xi_e(L/e)$。概率空间从未真的构造——恒等式由有限代数直接证明。用 $e\mid L$ 得每个乘积因子 $=\varphi_{\theta_e}(h/e)$（charfactor_eq，CircleMethodArcs.lean:95）。
把频率区间劈成 $\text{range }L=S_M\uplus S_m$：$S_M$（主弧）双射到标签窗 $[-N,N]$，$S_m$（次弧）是其余。分别估两块的和。
3. 主弧：Taylor → 高斯下界 $\ge c_3/\sigma_E$
方差尺度（CircleMethodMainTerm.lean:21）：$\sigma_E^2=\sum_e\dfrac{\theta_e(1-\theta_e)}{e^2}$，即 $\sum_e\xi_e/e$ 的方差；$\theta\in[1/3,2/3]$、$E$ 非空时每项 $\ge(2/9)/e^2>0$。
逐边 Bernoulli 对数 Taylor 展开 CircleMethodMainArc.lean:36
对 $\theta\in[1/3,2/3]$、$|t|\le1/10$：
$$\log\varphi_\theta(t)=2\pi i\,\theta t-2\pi^2\theta(1-\theta)t^2+R,\qquad\|R\|\le10^5|t|^3.$$
常数 $10^5$ 宽松但诚实（log 余项 $99000|t|^3$ + 匹配二次项 $1000|t|^3$）。
对边求和、取 $t_e=m/e$，用质量恒等式 $\sum_e\theta_e/e=1/b$ 把线性部分收成 $2\pi i(m/b)$、用 $\sigma_E^2$ 定义收二次部分（sum_logphi_bound，:89）：
$$\log\hat\mu(m)=2\pi i\tfrac mb-2\pi^2m^2\sigma_E^2+\delta_m.$$
对角项 $\text{term\_label}(m)=\hat\mu(m)e(-m/b)$ 相位抵消后是实高斯乘 $e^{\delta_m}$；当立方余项小（$\sum_e10^5|m/e|^3\le1/10$）时实部保留至少 $0.8$ 倍高斯（term_label_re_lower，:165）：
$$\mathrm{Re}\,\text{term\_label}(m)\ge0.8\,e^{-2\pi^2m^2\sigma_E^2}.$$
高斯和下界（纯分析） CircleMethodArcs.lean:350
窗口 $[-N,N]$ 上（$N\ge1/\sigma$）：$\displaystyle\sum_{|m|\le N}e^{-2\pi^2\sigma^2m^2}\ge\frac{e^{-\pi^2/2}}{2\sigma}$。证：保留 $[0,\lfloor1/(2\sigma)\rfloor]$ 里 $\ge1/(2\sigma)$ 个标签，各项 $\ge e^{-\pi^2/2}$。
主项下界
$$\mathrm{Re}\sum_{|m|\le N}\text{term\_label}(m)\ \ge\ \frac{c_3}{\sigma_E},\qquad c_3=0.8\cdot\frac{e^{-\pi^2/2}}{2}.$$
阶 $\asymp1/\sigma_E$，常数显式。主和还是实的（虚部为 0，由 $m\leftrightarrow-m$ 配对，term_label_sum_im_zero，:262）。再经 $S_M\leftrightarrow[-N,N]$ 双射转成频率和 main_sum_re_lower（:286）。
4. 次弧：字符衰减 → CRT 能量 $Q_E$
从 $|\varphi|^2\le1-4\theta_0(1-\theta_0)\sin^2\le e^{-4\theta_0(1-\theta_0)\sin^2}$，取平方根连乘（product_charFun_bound，BernoulliFourier.lean:72）：
$$|\hat\mu(h)|\le\exp\!\Big(-2\theta_0(1-\theta_0)\sum_e\sin^2(\pi h/e)\Big).$$
再用 Jordan 不等式 $\sin^2(\pi x)\ge4\|x\|^2$（sin_sq_pi_ge_four_nndist_sq），引入 CRT 能量 $Q_E(h)=\sum_e\|h/e\|^2$（QE，CircleMethodArcs.lean:28）：
字符衰减 → 能量 product_charFun_bound_QE · CircleMethodArcs.lean:75
$$|\hat\mu(h)|\le\exp\big(-8\theta_0(1-\theta_0)\,Q_E(h)\big).$$
在 $\theta_0=1/3$ 处常数 $=8\cdot\tfrac13\cdot\tfrac23=\dfrac{16}{9}$——这就是次弧到处出现的 $16/9$。
由三角不等式 $\|\sum_{h\in S_m}\text{fourierTerm}\|\le\sum_{h\in S_m}e^{-(16/9)Q_E(h)}$（minor_arc_norm_le，:114）。能量经频率→剩余映射 $h\mapsto(h\bmod p)_p$ 转成全局控制能量 $Q_{\mathrm{ctrl}}$（$Q_{\mathrm{ctrl}}(a(h))\le Q_E(h)$），得打包次弧界（minor_arc_bound，:304）：
次弧界（$o(1/\sigma)$）
$$\Big\|\sum_{h\in S_m}\text{fourierTerm}(h)\Big\|\le\frac{\eta+C_{\text{tail}}\,e^{-C^2(16/9)/2}}{\sigma_{\mathrm{ctrl}}}.$$
$\eta$ 取小、$C$ 取大即可压到 $<c_3/\sigma_E$。这里用到的全局控制分区定理 global_control_partition_final 是支柱二的心脏——见 次弧/SBEE 详解。频率映射的 $b$-对一重数由 mainArc_fiber_card_le（FiberCount.lean:69）给出。
5. 拍频收口 → Wcount>0
弧分离核 positivity_from_arcs · CircleMethod.lean:258
若 $L\cdot W=\text{main}+\text{minorSum}$，main 实且正，$\|\text{minorSum}\|\le\text{minorBound}<\text{main}$，则 $W>0$。（取实部：$\mathrm{Re}\,\text{minorSum}\ge-\text{minorBound}>-\text{main}$。）
实例化到 $S_M/S_m$（wcount_pos_of_split，CircleMethodAssembly.lean:24）：$\text{main}=\mathrm{Re}\sum_{S_M}$，$\text{minorSum}=\sum_{S_m}+i\,\mathrm{Im}\sum_{S_M}$。由主和虚部为 0，拍频 hbeat：
$$B_m<\frac{c_3}{\sigma_E}=\text{mainPos}\le\mathrm{Re}\sum_{S_M}\ \Longrightarrow\ 0<\mathrm{Wcount}.$$
图 · 主弧在 $m\equiv0$ 处形成高度 $\ge c_3/\sigma_E$ 的峰（蓝），次弧总贡献被压到 $B_m$（黄虚线）之下。拍频 hbeat 保证峰高压过次弧，从而 $\mathrm{Wcount}>0$。
汇成引擎主定理 exists_pos_weighted_of_construction（CircleMethodAssembly.lean:72）：吃 ArcConstruction 全部字段，吐 $0<\mathrm{Wcount}(E,\theta,b)$。