This is Paper 7 of a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography; Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Arbitrary-depth $k$-stage masked NTT pipelines with fresh inter-stage masking and per-stage PF-PINI($\leq 2$) gadgets satisfy a per-observation cardinality bound of $2 \cdot q^{2k-2}$ on the preimage of any output value, machine-checked in Lean 4 with zero \texttt{sorry}. Under the standard (informal) semantic translation that divides this cardinality by the total mask-tuple space size $q^{2k-1}$, the per-observation conditional probability bound is $2/q$, independent of pipeline depth $k$. The QANARY program has previously established machine-checked cardinality bounds on the per-observation leakage of masked NTT hardware: PF-PINI(2) for Barrett reduction (Paper 5 [3]), 2-stage composition with fresh inter-stage masking (Paper 6 [4]), an underlying universality theorem (Paper 3 [5]), and PF-PINI(1) for butterfly wires (Paper 4 [6]). This paper closes the program with four contributions. First, a $k$-stage composition theorem generalizing Paper 6's two-stage result to arbitrary $k \geq 1$ gives the last-stage-determined bound $G_{k-1}.\texttt{maxMult} \cdot q^{2k-2}$: only the last stage's PF-PINI parameter survives, with intermediate parameters erased by fresh inter-stage masking. Second, Montgomery reduction satisfies PF-PINI(2) with tight max-multiplicity 2. Third, we assemble these into the end-to-end bound $2 \cdot q^{2k-2}$ for any depth-$k$ PF-PINI($\leq 2$) pipeline under fresh inter-stage masking. Fourth, a Lean-verified hypothesis-violation conditional anchors the prior empirical and structural Adams Bridge analyses ([1, 2, 7, 8]).

翻译：本文是后量子密码学掩码NTT硬件形式化验证系列论文的第七篇。论文1[1]建立了QANARY平台的结构依赖分析，论文2[2]量化了部分NTT掩码下的安全裕度。任意深度k级掩码NTT流水线，采用级间新鲜掩码和每级PF-PINI(≤2)基本构件，满足任何输出值原像的每次观测基数上界为2·q^(2k-2)，该结论在Lean 4中经机器验证且不含任何`sorry`。根据标准（非形式化）语义转换，将此基数除以总掩码元组空间大小q^(2k-1)后，每次观测的条件概率上界为2/q，与流水线深度k无关。QANARY项目此前已建立掩码NTT硬件每次观测泄漏的机器验证基数界：Barrett约简的PF-PINI(2)性质（论文5[3]）、含级间新鲜掩码的两级组合（论文6[4]）、底层普适性定理（论文3[5]）以及蝶形连线的PF-PINI(1)性质（论文4[6]）。本文通过四项贡献完成该项目。第一，k级组合定理将论文6的两级结果推广至任意k≥1，得到末级决定界G_{k-1}.maxMult·q^(2k-2)：仅末级PF-PINI参数保留，中间参数被级间新鲜掩码消除。第二，Montgomery约简满足严格最大重数2的PF-PINI(2)性质。第三，我们将这些结果整合为任意深度k级PF-PINI(≤2)流水线在级间新鲜掩码下的端到端上界2·q^(2k-2)。第四，利用Lean验证的假设违反条件，锚定了先前的经验性与结构性Adams Bridge分析（[1,2,7,8]）。