Post-quantum cryptographic (PQC) accelerators for ML-KEM (FIPS 203) and ML-DSA (FIPS 204) rely on pipelined Number Theoretic Transform (NTT) stages over $\mathbb{Z}_q$. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. Whether per-stage arithmetic masking guarantees pipeline-level security had no prior machine-checked answer for the r-bearing case: composition frameworks (ISW, t-SNI, PINI, DOM) were formalized exclusively for Boolean masking over $\mathrm{GF}(2)$; no proof assistant artifact addresses the NTT butterfly over $\mathbb{Z}_q$. We present three machine-checked results in Lean 4 with Mathlib, all zero sorry. First, we close a stated limitation of prior work: value-independence implies constant marginal distribution under fresh randomness (via an algebraic MutualInfoZero proxy). Second, butterfly per-context uniformity: for any Cooley-Tukey butterfly with fresh output mask over $\mathbb{Z}/q\mathbb{Z}$ ($q > 0$), each output wire has exactly one mask value producing each output, a uniform marginal independent of secrets, universal over all moduli, twiddle factors, and inputs. Third, a k-stage NTT pipeline with fresh per-stage masking satisfies per-context uniformity at every stage under the ISW first-order probing model. We document a named warning: pointwise value-independence is false for butterfly outputs. The Adams Bridge accelerator (CHIPS Alliance Caliptra) fails the fresh masking hypothesis, masking active only in INTT round 0, architecturally explaining its structural insecurity. Artifact: nine theorems, 1,738 build jobs, zero sorry. Composition for nonlinear gadgets (Barrett) is addressed in forthcoming manuscripts proving Barrett's PF-PINI(2) satisfaction ('one-bit barrier') [3] and k-stage composition for PF-PINI gadgets under fresh-mask renewal [4].

翻译：面向ML-KEM（FIPS 203）与ML-DSA（FIPS 204）的后量子密码（PQC）加速器依赖于在 $\mathbb{Z}_q$ 上的流水线数论变换（NTT）级。我们先前的工作建立了大规模结构依赖性分析[1]，并量化了部分NTT掩码的安全裕度[2]。对于含r的情况，每级算术掩码能否保证流水线级安全性，此前尚无机器验证答案：组合框架（ISW、t-SNI、PINI、DOM）完全形式化于 $\mathrm{GF}(2)$ 上的布尔掩码；尚无证明助手工具处理 $\mathbb{Z}_q$ 上的NTT蝶形运算。我们利用Lean 4与Mathlib给出三项机器验证结果，均不含抱歉语句。首先，我们弥补了先前工作的已知局限：在新鲜随机性下，值独立性蕴含常数边际分布（通过代数MutualInfoZero代理）。其次，蝶形每上下文均匀性：对于任意带有新鲜输出掩码的Cooley-Tukey蝶形运算（模 $\mathbb{Z}/q\mathbb{Z}$，$q > 0$），每个输出导线恰有一个掩码值生成每个输出，该均匀边际分布独立于秘密，且对所有模数、旋转因子和输入普适。第三，在ISW一阶探测模型下，具有新鲜每级掩码的k级NTT流水线在每个阶段满足每上下文均匀性。我们记录了一个命名警告：蝶形输出的逐点值独立性不成立。Adams Bridge加速器（CHIPS Alliance Caliptra）不满足新鲜掩码假设，仅在INTT第0轮激活掩码，这从架构上解释了其结构性不安全。工件：九条定理、1738个构建任务、零抱歉语句。非线性基本门（Barrett）的组合方法将在后续手稿中阐述，证明Barrett满足PF-PINI(2)（“一位屏障”）[3]及新鲜掩码更新下PF-PINI基本门的k级组合[4]。