Exact Compilation and Resource Laws for Hidden Integer Feedback
Ganxuan Yang, Siqi Wen, Shuyan Yu, Jidong Yuan
cs.CR
Oct 19, 2026 · v1
TL;DR
Verifies the discrete-Gaussian mass, negative-floor arithmetic, hidden-rounding mixture and transcript semantics in Lean 4.19.0 with pinned Mathlib.
Abstract
Hidden randomized rounding couples the privacy loss of successive integer releases. We study a rational-feedback mechanism under predictable signed-unit participation and full observation of every physical output. A preparation's lifetime connects three results. First, preserving complete carries until an observed echo synchronizes the worlds gives exact finite-law point compilation, with support-width exponent $3C-2$ at every fixed budget $C\ge2$. Second, releasing commitments earlier gives a monotone hierarchy whose exact endpoint, strict gaps and numerical brackets quantify calibration loss. At one fixed discrete Gaussian, a loss allowance of 0.09 requires all four commitments. Third, legal regeneration yields an unrestricted KL rate with a square-root testing remainder and a complete asymptotic frontier under joint physical-time and participation constraints. At fixed rational parameters, finite-window occupation programs approximate that frontier to error $2^{-b}$ in polynomial bit time in $b$. Verified countable-transcript semantics and independently checked finite certificates support these analyses. A matched static workload illustrates the resulting design tradeoff: a structured finite integer matrix improves error and fresh randomness, while the scalar feedback instance retains fewer noise-state and source-table bits.
Problem
Hidden randomized rounding in integer-valued correlated-noise privacy mechanisms makes the privacy loss of successive releases depend on one another. Accounting must preserve this dependence across adaptive participations and finite physical horizons.
Approach
The authors study a rational-feedback mechanism with discrete Gaussian noise and hidden uniform rounding. They develop exact finite-law compilation by retaining complete carries until a synchronizing echo output. They define a monotone commitment-relaxation hierarchy and derive a KL participation rate and an asymptotic frontier under joint time and participation constraints. Kernel normalization, floor arithmetic, the hidden-rounding mixture and the countable-transcript semantics are verified in Lean against Mathlib, and finite certificates are checked independently.
Results
Exact compilation achieves support-width exponent 3C-2 and yields tight intervals for privacy profiles, for example Δ*_2(2)≈8.3992e-5. A loss allowance of 0.09 at one fixed discrete Gaussian requires all four commitments, and the asymptotic frontier can be approximated to error 2^{-b} in time polynomial in b.