本文是系列论文的第6篇，专注于后量子密码中基于数论变换（NTT）的掩码硬件的形式化验证。此前，布尔掩码的组成理论（如NI、SNI、PINI）已成熟，但素数域Z_q上的算术掩码（NTT后量子密码的基础）缺乏类似理论。本文首次提出了素数域上算术掩码的机器检查组合定理。核心洞察是“更新论证”（renewal argument）：在两个流水线阶段之间施加一个新鲜随机掩码时，中间线变得完全均匀，与第一阶段的安全参数无关。具体地，对于两个PF-PINI gadget（参数为k1和k2），如果组合时使用新鲜掩码，则两级流水线满足PF-PINI(k2)，第一阶段的多重性被完全消除；若没有新鲜掩码，中间线的多重性可达k1，为差分功率分析（DPA）创造必要条件。作者在Lean 4中形式化了两个定理，包含18个机器检查的证明，无任何“sorry”存根。他们还正式建立了Barrett约简的代数模型与硬件忠实模型之间的桥梁，并将定理实例化，用于诊断微软的Adams Bridge PQC加速器：缺乏级间新鲜掩码导致Barrett输出线在一阶探测模型下非均匀，这与两个独立的实证分析[3,4]及他们先前的结构分析[1]发现的架构缺陷一致。计算证据进一步表明，“1位屏障”（1-Bit Barrier）在Barrett和Montgomery约简中是普遍存在的。该工作为后量子密码掩码的形式化验证提供了关键理论基础，直接揭示了实际PQC硬件中的设计漏洞。

本论文针对后量子密码（PQC）硬件实现中的掩码Barrett reduction的侧信道泄漏问题，提出首个通用且机器验证的基数界限——1-Bit Barrier。Barrett reduction是基于NTT的PQC实现（如ML-KEM、ML-DSA）的非线性核心，但现有组合框架（ISW、t-SNI、PINI、DOM）仅针对GF(2)上的布尔掩码，无法直接应用于素域上的算术掩码。作者基于此前系列工作（QANARY、partial-NTT-masking margins、代数基础、蝴蝶组合），填补了这一空白。核心贡献在于：1）证明对于任意模数q>0和移位s，Barrett内部导线映射f_x(m) = ((x + 2^s - m) mod 2^s) mod q的原像基数属于{0,1,2}，绝不超过2——这一性质被称为1-Bit Barrier，意味着每条内部导线最多泄露1比特的最小熵；实际泄漏通常更少，因为计数为0的情况（不可达输出值）使界更为保守。2）引入PF-PINI（素域PINI）概念，证明Barrett满足PF-PINI(2)，Cooley-Tukey蝶形运算满足PF-PINI(1)，并观察到在阶段间加入新鲜掩码时，组合管线的最大原像基数为max(k1, k2)，因此1-Bit Barrier可传播。3）在Lean 4（Mathlib）中完成了12条定理的机器验证，无一个“sorry”，结果对所有q>0通用。4）指出Adams Bridge因缺少阶段间新鲜掩码而违反PF-PINI组合，解释了此前发现漏洞的原因。该工作为NIST IR 8547推荐的形式化方法在PQC实现验证中提供了首个通用机器验证的基数界，并给出1比特泄漏的直观解释。适合侧信道分析、PQC硬件安全、形式化验证领域的研究者和工程师阅读。