从有限枚举到通用证明：面向 PQC 硬件掩码验证的环论基础

PQC 硬件掩码的形式化验证依赖于有限域上的 SMT 求解器。我们之前的工作在大规模建立结构依赖分析 [1] 并量化部分 NTT 掩码的安全裕度 [2]。QANARY——我们的结构依赖分析框架——已验证了阿德斯斯桥 ML-DSA/ML-KEM 加速器 [3, 4] 中的 117 万个单元跨 30 个模块，但其核心正确性结果（定理 3.9.1）仅在 $q = 5$ 时通过 $2^{25}$ 个布尔线路函数进行机器检查。这留下了对 ML-KEM（$q = 3{,}329$，FIPS 203 [5]）和 ML-DSA（$q = 8{,}380{,}417$，FIPS 204 [6]）的可移植性作为开放问题。NIST IR 8547 [7]（2025 年 3 月）促使关闭此类差距。我们提出了 Theorem 3.9.1 中 $r$-free 子定理的首个机器检查普遍证明：对于任意 $q > 0$、任意线路函数和任意两组密钥，价值独立性意味着相同边际分布。该证明在 Lean 4 [8] 中完成，配合 Mathlib [9]，仅需五行代码，而非 $2^{25}$ 次有限评估。它无需 apology，减少了信任基线从 {Z3 [10], CVC5 [11], Python} 到 Lean 4 内核。我们提供九个定理（T1--T6, T1', T3'）涵盖再参数化、双射性、溢出界限、RNG 偏置以及所有 $q \geq 2$ 的通用非紧致性反例。结果表明 $\mathbb{Z}/q\mathbb{Z}$ 的交换环公理是算术掩码验证的自然抽象层。