Barrett reduction is the nonlinear core of every practical NTT-based post-quantum cryptography implementation. Existing composition frameworks (ISW, t-SNI, PINI, DOM) address Boolean masking over GF(2); none provides a machine-checked characterization of Barrett's leakage under first-order arithmetic masking and the first-order probing model over prime fields. Building on our prior series, QANARY [15], partial-NTT-masking margins [14], algebraic foundations [16], and butterfly composition [18], we close this gap. We prove a trichotomy: for any $q > 0$ and shift $s$, the Barrett internal wire map $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ has preimage cardinality in $\{0, 1, 2\}$, never more. We call this the 1-Bit Barrier: max-multiplicity 2 implies at most 1 bit of min-entropy loss per internal wire, universal over all moduli. The count-zero cases, unreachable output values, reveal that actual leakage is often strictly less than 1 bit, making the bound conservative. We introduce PF-PINI (Prime-Field PINI): Barrett satisfies PF-PINI(2); the Cooley-Tukey butterfly satisfies PF-PINI(1). We observe (not yet proved) that with fresh inter-stage masking, the composed pipeline has max-multiplicity $\max(k_1, k_2)$, so the 1-Bit Barrier propagates. The trichotomy, the PF-PINI instantiations, and cardinality results are machine-checked in Lean 4 with Mathlib: 12 proved results, zero sorry, universal over all $q > 0$ (the min-entropy bound follows by standard definitions). Adams Bridge lacks fresh inter-stage masking, violating PF-PINI composition and explaining why Papers 1 [15] and 2 [14] found vulnerabilities. NIST IR 8547 recommends formal methods for PQC implementation validation. The 1-Bit Barrier provides the first universal machine-checked cardinality bound for masked Barrett reduction in ML-KEM (FIPS 203) and ML-DSA (FIPS 204), with a corresponding 1-bit leakage interpretation.

翻译：Barrett归约是每个基于NTT的实用后量子密码实现的非线性核心。现有组合框架（ISW、t-SNI、PINI、DOM）处理的是GF(2)上的布尔掩码；尚未有框架能在素数域上一阶算术掩码和一阶探测模型下，对Barrett的泄漏给出机器可校验的表征。基于我们先前的研究系列——QANARY [15]、部分NTT掩码余量 [14]、代数基础 [16] 和蝶形组合 [18]，我们填补了这一空白。我们证明了一个三分律：对于任意 $q > 0$ 和移位量 $s$，Barrett内部导线映射 $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ 的原像势属于 $\{0, 1, 2\}$，绝不超过2。我们称此为1比特屏障：最大重数为2意味着每条内部导线最多损失1比特的最小熵，对所有模数普适成立。零个原像的情况（即不可达输出值）表明，实际泄漏通常严格小于1比特，因此该界是保守的。我们引入了PF-PINI（素数域PINI）：Barrett满足PF-PINI(2)；Cooley-Tukey蝶形满足PF-PINI(1)。我们观察到（尚未证明）若采用级间新鲜掩码，组合流水线的最大重数为 $\max(k_1, k_2)$，因此1比特屏障得以传播。该三分律、PF-PINI实例化以及势结果已在Lean 4与Mathlib中机器校验：12个已证结果，零个未完成证明，对所有 $q > 0$ 普适成立（最小熵界遵循标准定义）。Adams Bridge缺少级间新鲜掩码，违反了PF-PINI组合，这也解释了论文1 [15] 和论文2 [14] 发现漏洞的原因。NIST IR 8547建议对PQC实现验证采用形式化方法。1比特屏障为ML-KEM（FIPS 203）和ML-DSA（FIPS 204）中的掩码Barrett归约提供了首个通用机器校验势界，并对应1比特泄漏的解释。