论文提出用矩阵刷新实现抗泄露计算并给出 Lean 4 形式化

论文证明一种简单刷新方式在持续局部泄露下是安全的：左方将份额乘以可逆矩阵 M，右方乘以 M 的逆矩阵 M⁻¹。经过 T 次刷新、每次每方最多泄露 λ 比特后，两个被存储秘密的转录统计距离至多为 C·T·2^{6λ-n/9}，C 为绝对常数。