Differential Privacy

[DavidLedvinka]

RandomDo now has a differential privacy foundation and Gaussian mechanisms written as polymorphic rdo programs. The scalar and vector mean samplers compute the empirical mean and add Gaussian noise with standard deviation proportional to the public domain diameter and inversely proportional to a public minimum dataset size.

• Define arbitrary-length datasets, add/remove and replacement adjacency, probability-valued mechanisms, pure DP, and approximate DP, with deterministic postprocessing and budget monotonicity.
• Prove empirical-mean sensitivity in the ℓ₂ norm, Gaussian privacy bounds, and calibration for all positive ε and 0 < δ ≤ 1, including zero diameter.
• Prove the exact laws of the same rdo samplers and certify their (ε, δ)-DP guarantees under both adjacency relations. Add formal examples, seeded execution checks, and usage documentation.

The privacy guarantee concerns the exact real interpretation. The existing floating-point backend executes the same programs for simulation; its rounding and generator are outside this guarantee. Diameter and minimum size are public bounds.

Validation: lake build RandomDo Test passes on the original Lean 4.34.0-rc2 development checkout. All new privacy proofs use only the standard Lean axioms, with no sorry or custom axioms. The module import indexes include all new files. GitHub CI is validating current main (Lean 4.35.0-rc4); a local check on that version was not completed because its dependency cache download was too slow.