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.

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