← All papers
First page of Exact Compilation and Resource Laws for Hidden Integer Feedback

Exact Compilation and Resource Laws for Hidden Integer Feedback

Ganxuan Yang, Siqi Wen, Shuyan Yu, Jidong Yuan

cs.CR Oct 19, 2026 · v1
Verifies the discrete-Gaussian mass, negative-floor arithmetic, hidden-rounding mixture and transcript semantics in Lean 4.19.0 with pinned Mathlib.
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.

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.

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.

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.