圆法要成立，必须证明“非对角频率”（次弧）贡献的总质量远小于主弧尺度 $1/\sigma$。这是整个证明最难、代码量最大的部分。本页讲两件事：(1) 全局控制分区定理 global_control_partition_final 如何把次弧质量压到 $o(1/\sigma)$；(2) SBEE（单块能量–熵）如何用一条确定性的区间计数引理（Lemma D）无条件成立——完全不需要 Irving 的 Kloosterman 界。
single_block_counting），靠的是“一个剩余类在 dyadic 区间里至多命中 2 个点”的初等事实，不是 Kloosterman。整个 15 文件解析核心：0 个代码 sorry、0 条 axiom；全树信任基仅两条 Rosser–Schoenfeld 公理。
核心是“最近整数”核 $\|x\|=$ nndist1（GlobalControl.lean:75）与频率能量
$$Q_E(h)=\sum_{e\in E}\Big\|\frac he\Big\|^2\quad(\texttt{QE},\ \text{CircleMethodArcs.lean:28}).$$
它经 Jordan 桥 $\sin^2(\pi x)\ge4\|x\|^2$（sin_sq_pi_ge_four_nndist_sq）控制乘积字符和衰减：$\big|\prod\text{charFun}\big|\le e^{-8\theta_0(1-\theta_0)Q_E}$。在 $\theta_0=1/3$ 处 $8\theta_0(1-\theta_0)=16/9$——这就是后面反复出现的常数 $c=16/9$。
把频率 $h$ 映成剩余向量 $a(h):p\mapsto(h\bmod p)$。定义控制能量（GlobalControl.lean:183）与尺度（:188）：
Qctrl BS a = ∑_{(p,q)∈ctrlPairs} (H_{p,q}(a)/(pq))²
sigmaCtrl BS = √( ∑_{(p,q)∈ctrlPairs} 1/(pq)² )$H_{p,q}(a)=$ crtRepr 是 $(a_p,a_q)$ 的中心化 CRT 解（$|H|\le pq/2$，$p,q$ 不互素时为 0），即两个剩余的“拍频”。$\sigma_{\mathrm{ctrl}}$ 是把所有分子换成 1 的“单位格”尺度，它决定主弧宽度 $\sim1/\sigma$。$\sigma_{\mathrm{ctrl}}>0$ 已证（GlobalControlG7.lean:263）。
ctrlEdges BS ⊆ E 时，$Q_{\mathrm{ctrl}}(a(h))=\sum_{pq\in\text{ctrlEdges}}\|h/(pq)\|^2\le Q_E(h)$。因为控制边 $pq$ 的中心化 CRT 分子恰是 $\|h/(pq)\|$ 的分子。于是字符和衰减 $e^{-cQ_E}\le e^{-cQ_{\mathrm{ctrl}}}$，控制 $\sum e^{-cQ_{\mathrm{ctrl}}}$ 就控制了次弧质量。下游以 $c=16/9$ 调用。主弧（GlobalControl.lean:1872）= 全局对角、且标签小的剩余向量：$\{a\mid\exists m,\ |m|\le C/\sigma_{\mathrm{ctrl}},\ \forall p,\ a_p=m\bmod p\}$。定理说：离开主弧的总质量里，$\eta$ 项可做到任意小（被 floor 吸收），$C_{\text{tail}}e^{-C^2c/2}$ 项是超出半径 $C$ 的一维高斯尾——两项都是 $o(1/\sigma_{\mathrm{ctrl}})$。
floor 是两种独立惩罚取小（GlobalControlG6.lean:35）：
| 惩罚 | 量级 | 来源 |
|---|---|---|
| 每块 forcing floor $R_w$ | $c_2\cdot 2^k/(\log 2^k)^3$ | 某块非 $m$-主导 ⟹ 被迫付能量（Theorem B） |
| 边界惩罚 $\Pi_{\text{floor}}$ | $\dfrac{(|P_{k+1}|-e_0-1)(|P_k|-e_0)^3}{2^{13}(2^k)^2}$ | 两相邻“冷块”带不同标签 ⟹ 二部交叉能量 $X_{en}$ |
证明三分（:413 起）：① 有“热块”（能量 $\ge R_w$）⟹ floor；② 有“边界集”（相邻冷块标签不同）⟹ $\Pi_{\text{floor}}\le X_{en}\le Q_{\mathrm{ctrl}}$ ⟹ floor；③ 否则全部冷块共享同一标签 ⟹ 全局对角，由 diagonal_Qctrl（:230：全局对角 + $2|m|<pq$ ⟹ $Q_{\mathrm{ctrl}}=m^2\sigma^2$）落入 diagSector；又因 $a\notin$ 主弧，必有 $|m|>C/\sigma$。
diagSector（:40）：全局对角、$|m|>C/\sigma$、且能量恰为 $Q_{\mathrm{ctrl}}=m^2\sigma^2$——正是喂给 Sector-II 一维高斯尾的那批。
三个因子各有含义：$e^{A\cdot\text{numBlocks}}$ 是熵预算（每块常数个标签模式，Peierls 论证要对抗的指数因子——这也是为什么 admissibleGlobalRange 要把块数压成 $O(k_0)$ 线性）；$e^{8\varepsilon R}$ 是可调 Laplace 松弛（$\varepsilon$ 任意小，后面在 Sector-I 里让 $8\varepsilon<c$）；$1+\sqrt R/\sigma$ 是一维标签体积。
GlobalPeierlsBookkeeping.lean，纯有限组合，163 行全证）核心引理 weighted_subset_entropy（:35）：只要每块代价 $\text{cost}_i\le e^{\varepsilon w_i/4}$，则
$$\sum_{S:\ \sum_{i\in S}w_i\le R}\ \prod_{i\in S}\text{cost}_i\ \le\ e^{\varepsilon R/2}\cdot e^{\sum_i e^{-\varepsilon w_i/4}}.$$
即：给每个偏离块按 $\varepsilon/4$ 的率“收”一片能量，就把“选哪些块偏离、怎么偏离”的熵吸收进一个全局能量折扣 $e^{\varepsilon R/2}$ 乘可收敛的局部配分函数积。配套 segment_label_constant（:150）：冷段上标签恒定，整段只算一次标签选择。
SBEE = Single-Block Energy–Entropy。历史上曾以 ConditionSBEE（SBEE.lean:84）作为假设喂给圆法，且那条老路径依赖 Irving 的 Kloosterman 界。现在它是无条件定理，而且证明是初等确定性的。
SBEEPartitionBound c 成立：存在一个常数 $C$（量词在 $\forall P$ 之外）使得对每个满足 IrvingGood 的素数块 $P$（$|P|\ge2$）：$\displaystyle\sum_a e^{-c\,Q_P(a)}\le C/\sigma_P$。IrvingGood P（SBEEAssembly.lean:40）尽管名字叫 “Irving”，实际是纯 dyadic 密度条件：$P$ 是窗口 $[X,2X]$ 内密度 $\ge X/(2\log X)$ 的素数集——正是 BlockSystem.hdensity 提供的东西。不需要任何 Kloosterman 输入。
核心事实 lemmaD_fiber：一个固定的模 $q$ 剩余类，与 dyadic 区间 $[X,2X]$ 至多相交 2 个点——纯粹因为区间长度 $X\le q$。这条初等区间计数完全替代了 Irving 的 Kloosterman 界。由它得色散能量下界 dispersion_energy_bound（:270，以 ring 收尾）：$\sum_{p\in F}(\text{phase})^2\ge|F|^3/(2^{11}X^2)$。
SBEEForcing.lean，1892 行）| 定理 | 陈述 | 状态 |
|---|---|---|
Theorem Atheorem_A_dominant_count :783 | 主导配置（单一小标签 $m$ 被 $(1-\rho)$ 比例素数共享）本质一维，计数 $\sim\sqrt R/\sigma_P$，无熵爆炸。 | 已证 |
Theorem Btheorem_B_nondominant_forcing :1562 | 任何非主导配置被迫付能量 $\ge c_2 X/(\log X)^3$——即 G6 用的每块 floor $R_w$。 | 已证 |
Lemma Elemma_E_cross_label_energy :422 | 两个不同标签类 $C,C'$ 产生 CRT 能量 $\ge c|C|^3|C'|/X^2$（$c=1/8192$）；“无法廉价持有两个标签”。喂给 Theorem B。 | 已证 |
Theorem Cfingerprint_count :732 | 网格窗口之上，水平集计数 $\le|P|\cdot e^{\varepsilon R}$，线性于 $|P|$、无指数熵。 | 已证 |
unified_levelset（SBEEAssembly.lean:133）在网格尺度 $X^{2/3}$ 处劈开：窗口之下合用 Theorem A + B，之上用 Theorem C（fingerprint），由 mesh_lemma 缝合，再经 partfun_series_bound（Laplace/几何优超）得 single_block_counting。
IrvingKloostermanBound'（SBEE.lean:115）只出现在已废弃的 SBEE.lean 和老的条件路径 MainTheorem.lean:109（erdos_306_conditional）里。无条件路径 Erdos306Final.lean 不用它。真正的 SBEE 证明是确定性的（Lemma D），Kloosterman 不在关键路径上。
hbeat合同要 $\|\sum_{S_m}\text{fourierTerm}\|\le B_m<c_3/\sigma_E$。由 $\|\sum\|\le\sum\|\cdot\|$，把 $S_m$ 覆盖成 $S_{\text{block}}\cup S_{\text{extra}}$，两条 lane 各自估：
global_control_partition_final（$c=16/9$），得 $B_m$ 的第一括号 $\big(b\eta+bC_{\text{tail}}e^{-C^2(16/9)/2}\big)/\sigma$。hbeatr2_close_budget_501 给 $B_m<c_3/(501\sigma)$，再由 $\sqrt{\mathrm{sigmaE2}}\le501\sigma$ 抬成 $B_m<c_3/\sigma_E$ = hbeat。主项压过次项，Wcount>0。sorry（GlobalControl.lean:778）在 /- … -/ 注释块内，标注为“ORIGINAL STATEMENT, FALSE”；真正的 mismatch_penalty 在 :792 已证。dispersion_energy_bound 以 ring 收尾）。信定理声明，别信散文。_final 版本。活跃链一律走 global_control_partition_final、global_levelset_final；无后缀的同名在当前树里根本不是定理。RSPrimeSums.lean:41,59）+ Lean 三逻辑原语。详见 公理页。子 agent 的审计为源码级（声明 + 注释剥离）分析；机器核验请跑 Audit.lean 的 #print axioms erdos_306。