Constant Mechanisms🔗

A mechanism that ignores its input has the same output distribution on every neighboring pair. It therefore satisfies pure privacy with zero budget:

The proof is simp because after intro the goal is \mu(S)\le e^0\cdot\mu(S)+0, and e^0=1. Both sides concern the same event under the same measure. PureDP is the \delta=0 abbreviation.

Note which quantifier order made this easy. Privacy is universally quantified over adjacent pairs and over measurable events, so intro a a' _ S _ discharges all five binders and leaves an arithmetic goal. The proof works for any probability measure on the output space.

Monotonicity Of The Budget🔗

Two closure facts get their own theorems. The first, differentialPrivacy_mono_delta, says a mechanism private for \delta_1 is private for any looser \delta_2\ge\delta_1. The second allows the same relaxation of \varepsilon:

@differentialPrivacy_mono_eps : ∀ {α β : Type} {Adj : α → α → Prop} [inst : MeasurableSpace β] {M : Mechanism α β}
  {ε₁ ε₂ : ℝ} {δ : ENNReal}, ε₁ ≤ ε₂ → DifferentialPrivacy Adj M ε₁ δ → DifferentialPrivacy Adj M ε₂ δ

Together the two lemmas say the predicate is monotone in the whole budget (\varepsilon,\delta). A caller may therefore use a looser budget than the one already proved. For the epsilon lemma, monotonicity of \exp increases the multiplier on the right-hand side; multiplying a nonnegative event probability preserves that inequality. This is the comparison handled by gcongr.

For example, a proof at (0.5,0) can be reused at (1,0) by supplying the real inequality 0.5\le1. The theorem keeps the mechanism and adjacency fixed. It does not describe the budget of two successive releases: comparing two numbers on the right-hand side of one event inequality is different from analyzing a joint output distribution. In Lean, the two arrows in the signature make the use explicit: first give the budget comparison, then the existing privacy proof, and the result is the relaxed privacy proof.

Postprocessing🔗

@differentialPrivacy_postprocess : ∀ {α β γ : Type} {Adj : α → α → Prop} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {M : Mechanism α β} {ε : ℝ} {δ : ENNReal} {f : β → γ} (hf : Measurable f),
  DifferentialPrivacy Adj M ε δ → DifferentialPrivacy Adj (postprocess M f hf) ε δ

Here f is a fixed measurable function of the released output. It may, for example, convert a private model into an exported representation or a report. Applying it preserves the budget, provided it uses only the released output and fixed public information. An evaluator that reads the private dataset again is outside this theorem.

The proof is short for a mathematical reason. For a measurable output event T, the post-processed mechanism lands in T exactly when the original mechanism lands in the measurable preimage f^{-1}(T). Applying the DP inequality to that preimage gives

\begin{aligned} \Pr[f(M(D))\in T] &=\Pr[M(D)\in f^{-1}(T)]\\ &\le e^\varepsilon\Pr[M(D')\in f^{-1}(T)]+\delta\\ &=e^\varepsilon\Pr[f(M(D'))\in T]+\delta. \end{aligned}

A useful model example is a private vector of weights followed by a fixed prediction rule at a public input. Here β is the weight space, γ is the prediction space, and f performs inference at that input. An event such as “the prediction is class 2” becomes the set of weights for which inference returns class 2. Privacy of the weights already bounds the probability of that set. This explains why the proof uses preimages: the two spaces can have quite different representations, but the probability comparison is still about the original release.

The measurability hypothesis hf licenses the preimage step. Together with the original privacy premise, it is sufficient; the proof does not inspect the representation of the model or report. The reference point is the event inequality of Dwork et al. (2006).

Sampling And Privacy Guarantees🔗

Sampling alone cannot establish the universally quantified privacy predicate. The same limitation affects robustness and asymptotic stability: finite experiments test cases, not all quantified inputs.

Take the Laplace mechanism on a counting query. Two adjacent datasets differ in one record, so the count differs by at most the sensitivity \Delta=1. Releasing the count plus \mathrm{Laplace}(0,\Delta/\varepsilon) noise is (\varepsilon,0)-DP. With \varepsilon=0.5 the noise scale is 2. Take the true counts 10 and 11, and the tail event S=\{\text{output}\ge 12\}, which is the direction that favors the larger count and is therefore where the inequality is tightest. Two million samples per dataset in PyTorch (Paszke et al., 2019):

# Compare one Laplace tail event in both directions of
# dataset adjacency.
import torch, math
torch.manual_seed(0)
lap = torch.distributions.Laplace(torch.tensor(0.), torch.tensor(2.))
zD  = 10. + lap.sample((2_000_000,))
zDp = 11. + lap.sample((2_000_000,))
pD  = (zD  >= 12.).float().mean().item()
pDp = (zDp >= 12.).float().mean().item()
print(f"P[M(D)>=12]  emp {pD:.5f}  exact {0.5 * math.exp(-1):.5f}")
print(f"P[M(D')>=12] emp {pDp:.5f}  exact {0.5 * math.exp(-0.5):.5f}")
print(f"ratio D/D'   {pD / pDp:.5f}")
print(f"ratio D'/D   {pDp / pD:.5f}")
print(f"e^eps        {math.exp(0.5):.5f}")

P[M(D)>=12]  emp 0.18385  exact 0.18394
P[M(D')>=12] emp 0.30330  exact 0.30327
ratio D/D'   0.60618
ratio D'/D   1.64968
e^eps        1.64872

The exact tail probabilities are \tfrac12 e^{-1} and \tfrac12 e^{-1/2}, and their ratio is exactly e^{1/2}, so this event attains the privacy bound in the direction from the larger count to the smaller one.

Now look at the last three lines again. The empirical ratio is 1.64968 and the bound is e^{0.5}=1.64872. The estimate violates the inequality it is supposed to illustrate, by about six parts in ten thousand, because each probability was estimated from a finite sample. More samples can improve estimates for this fixed event, but cannot establish the inequality for every measurable event and every neighboring pair. Rare events are especially difficult to estimate: few or no sampled outputs may land in them. The analytical tail calculation explains this experiment; a privacy proof must cover the full quantification.

Privacy Verification Gaps🔗

No privacy budget should be inferred from the presence of the DP namespace. The current source supplies the semantic target and the closure laws. It does not contain a runtime privacy accountant, a calibration theorem for the Laplace or Gaussian mechanism, a composition theorem, or an end-to-end theorem for a training command. Concretely, the gap between this file and a DP-SGD claim is: Poisson or uniform subsampling with its amplification argument, per-example gradient clipping with a sensitivity bound, noise calibration to that sensitivity, and composition accounting across steps. Each of those is a separate implementation and proof obligation. What the file does give you is the target they must hit, plus the measurable, data-independent post-processing theorem.

Tensor Norms And Perturbation Balls🔗

Everything on the runtime side is ordinary executable code. Here is a two by two linear map, its output, and the two norms:

[4.000000, 2.000000]

4.000000

4.472136

1.000000

false

The first output is W(1,1)^\top=(3+1,0+2)^\top=(4,2)^\top, whose \ell^\infty norm is the larger absolute coordinate 4 and whose \ell^2 norm is \sqrt{20}\approx4.4721360. The inputs (1,1) and (0,1) differ only in the first coordinate, so their distance is 1 in every \ell^p. And (0,1) is not in the \ell^\infty ball of radius 0.5 around (1,1), because 1>0.5, so the ball test returns false.

The ball test checks whether this pair satisfies the proposed perturbation constraint. Its norm and radius must match the ones used by a robustness theorem.

The corresponding PyTorch calculation prints the same values:

# Compute the same linear output and norms with PyTorch
# tensors.
W = torch.tensor([[3., 1.], [0., 2.]])
x = torch.tensor([1., 1.])
print("f(x)      ", (W @ x).tolist())
print(f"linf f(x)  {torch.linalg.vector_norm(W @ x, float('inf')).item():.6f}")
print(f"l2   f(x)  {torch.linalg.vector_norm(W @ x).item():.6f}")

f(x)       [4.0, 2.0]
linf f(x)  4.000000
l2   f(x)  4.472136

The choice of ball has a direct geometric effect. Around (1,1), the infinity-norm ball of radius 0.5 allows each coordinate to move independently by at most 0.5. Its corner (1.5,1.5) is at Euclidean distance \sqrt{0.5} from the center, so it is outside the Euclidean ball with the same numeric radius. A radius therefore needs its norm to be meaningful. For a model whose input is normalized before inference, the tensor in the theorem is the input at that stage; a radius in normalized coordinates requires a conversion before it describes a perturbation of raw pixels or physical measurements.

Empirical Lipschitz Ratios🔗

The runtime layer also provides empirical helpers: Lipschitz ratios over a finite set of input pairs, and deterministic perturbation sampling. Changing the sampled direction changes the observed gain, even for this two-dimensional linear map:

Except.ok 3.000000

Except.ok 3.256617

The first pair differs in the first coordinate, so it measures the gain on (1,0)^\top, which is \|(3,0)^\top\|_2=3. The second pair approximates the top singular direction. The spectral norm, with its decimal expansion rounded, is \sigma_{\max}(W)=\sqrt{7+\sqrt{13}}\approx3.2566165. In exact arithmetic, ratios at distinct points lower-bound the least Lipschitz constant. Here the direction and arithmetic are rounded, so the diagnostic is an approximation, not a proved lower bound. The second direction closely approximates the maximizing singular vector.

# Compare the sharp spectral constant with the Frobenius
# upper bound.
print(f"spectral norm {torch.linalg.matrix_norm(W, 2).item():.6f}")
print(f"frobenius     {torch.linalg.matrix_norm(W, 'fro').item():.6f}")

spectral norm 3.256617
frobenius     3.741657

For the first sampled direction, the exact ratio, spectral norm, and Frobenius norm have the following order:

\underbrace{3}_{\text{sampled pair}} \;\le\; \underbrace{\sqrt{7+\sqrt{13}}}_{\sigma_{\max}(W),\ \text{least Lipschitz constant}} \;\le\; \underbrace{\sqrt{14}}_{\|W\|_F,\ \text{Frobenius bound}}.

The middle number is what a robustness argument would like to use. The right number is what linear_layer_lipschitz_bound in MlpRobustness proves, by bounding the operator norm with the Frobenius norm. The squared Frobenius norm is the sum of squared entries, so a Cauchy-Schwarz argument gives the bound without computing singular values. The resulting bound is loose by about 15\% on this matrix and can be loose by a factor of \sqrt{\min(m,n)} in general. If a downstream certificate ever needs the sharper constant, that is a new theorem, not a new diagnostic.

The wrapper Except.ok says that the ratio computation returned a result through its success branch. The number inside is still the ratio for the supplied pairs. To use the Frobenius upper bound in this example, one instead reasons about an arbitrary displacement v: each output coordinate is a row dot product, Cauchy–Schwarz bounds its square, and summing the row bounds gives \|Wv\|_2^2\le\|W\|_F^2\|v\|_2^2. The bias disappears when subtracting two outputs. This proof covers directions absent from the sample array, which is precisely the information a robustness certificate needs.

There is a related helper for one-directional sensitivity:

3.000000

This computes the finite-difference ratio \|f(x+p)-f(x)\|_2/\|p\|_2. Over the reals, for a linear map and a fixed nonzero direction, the ratio is independent of step size. For a nonlinear network it may also vary with the point and step size. In either case, floating subtraction of nearby outputs can lose precision.

Lipschitz Bounds And Margin Certificates🔗

The implications needed to turn a Lipschitz bound into a robustness certificate are proved in LipschitzCertified. The first step turns a Lipschitz bound into an output-perturbation bound:

@is_adversarially_robust_of_lipschitz : ∀ {s₁ s₂ : Shape} {f : Tensor ℝ s₁ → Tensor ℝ s₂}
  {norm₁ norm₂ : {s : Shape} → Tensor ℝ s → ℝ} {L : ℝ},
  0 ≤ L →
    isLipschitzContinuous f (fun {s} => norm₁) (fun {s} => norm₂) L →
      ∀ (x₀ : Tensor ℝ s₁) (ε : ℝ), IsAdversariallyRobust f (fun {s} => norm₁) (fun {s} => norm₂) x₀ ε (L * ε)

Read the conclusion: the output radius is L\varepsilon, with no hypothesis on \varepsilon beyond what isLipschitzContinuous already gives. For an input satisfying the ball premise, multiply its distance bound by the nonnegative Lipschitz constant. This bounds output drift; preserving a label also requires a margin between logits.

The second step is about labels, and it needs a quantity the drift bound does not mention: how far ahead the winning logit is.

@HasLogitMargin : {n : ℕ} → Tensor ℝ [n] → Fin n → ℝ → Prop

HasLogitMargin y c m says class c beats every competitor by at least m. Combining the two gives the classical margin-over-Lipschitz certificate:

@is_certified_robust_of_lipschitz_of_logitMargin : ∀ {s₁ : Shape} {n : ℕ} {f : Tensor ℝ s₁ → Tensor ℝ [n]}
  {normIn : {s : Shape} → Tensor ℝ s → ℝ} {L : ℝ},
  0 ≤ L →
    isLipschitzContinuous f (fun {s} => normIn) (fun {s} => tensorLinfNorm) L →
      ∀ {x₀ : Tensor ℝ s₁} {ε m : ℝ} {c : Fin n},
        0 ≤ ε →
          0 < m →
            HasLogitMargin (f x₀) c m →
              2 * (L * ε) < m → IsCertifiedRobust (fun x => argmaxClassifier (f x)) (fun {s} => normIn) x₀ ε

The side condition is 2L\varepsilon<m. The winning logit can fall by L\varepsilon while a competitor rises by L\varepsilon, so the gap can close at twice the drift rate. For L>0, this becomes \varepsilon<m/(2L), which is why a loose Lipschitz constant costs radius linearly, and why the 15\% gap between \|W\|_F and \sigma_{\max}(W) above reduces the certified radius.

Note also that the output norm in this theorem is pinned to \ell^\infty while the input norm normIn stays free. That asymmetry is forced by the proof: the margin argument compares individual logits, and the norm that controls individual coordinates is the sup norm. The companion lemma is_lipschitz_continuous_linf_of_l2 in the same file is what lets an \ell^2 bound be fed into this slot.

The strict inequality in the margin condition removes ties. If the gap could shrink exactly to zero, the classifier's tie-breaking convention would become relevant. With a positive remaining gap, every competitor is strictly below c, so the same class is selected regardless of that convention. The conclusion IsCertifiedRobust compares the prediction throughout the ball with the prediction at its center. It does not compare either prediction with an external ground-truth label. To state robust accuracy, a caller also supplies the fact that the center's predicted class is the intended label.

Logit-Margin Certificate Example🔗

For a concrete certificate, start at logits (2,0) with margin 2 and the identity map as the classifier's tail, so L=1:

The margin proof is two cases because HasLogitMargin quantifies over competitors: fin_cases k splits on the class index, the winning class is excluded by the hypothesis k ≠ c, and the competitor obligation is 0\le 2-2, which norm_num closes after unfolding the literal. That unfolding works because getScalar_ofList is a simp lemma, so a rank-one tensor literal reduces to list lookup without any manual Rep reasoning.

The three by norm_num arguments at the end are the numeric side conditions: 0\le 0.4, 0<2, and 2\cdot(1\cdot 0.4)=0.8<2. The last one is the certificate. It is also where the radius stops: at \varepsilon=1.2 the same call fails, because 2\cdot(1\cdot 1.2)=2.4 is not below the margin 2. A failed sufficient condition alone does not establish the existence of an adversarial example at radius 1.2. For this identity map, we can supply a separate witness: (0.8,1.2) is within radius 1.2 of (2,0) and class 1 wins. That witness supplies the information that failure of a sufficient condition alone would not.

Within radius 0.4 in the infinity norm, each logit can move by at most 0.4. The worst change for the predicted class lowers its logit and raises its competitor, reducing the gap from 2 to at least 1.2. This calculation explains the factor of two in the general condition. For an earlier layer of a model, the Lipschitz bound first converts an input perturbation radius into this bound on logit movement.

MLP Lipschitz Bounds🔗

The same machinery composes to a network, in MlpRobustness:

@NN.MLTheory.Proofs.mlp_is_lipschitz_continuous_l2 : ∀ {inDim hidDim outDim : ℕ} (l1 : LinearSpec ℝ inDim hidDim)
  (l2 : LinearSpec ℝ hidDim outDim),
  l1.weights ≠ Tensor.full [hidDim, inDim] 0 →
    l2.weights ≠ Tensor.full [outDim, hidDim] 0 →
      ∃ L > 0,
        isLipschitzContinuous (fun x => Examples.mlpForward l1 l2 x) (fun {s} => Proofs.tensorL2Norm)
          (fun {s} => Proofs.tensorL2Norm) L

The conclusion is existential, so using it in a certificate means obtaining a witness L and its Lipschitz proof. The constant it is built from is the product of the two Frobenius norms, and the proof shows that product works, but the statement does not export the formula. The nonzero-weight hypotheses are there because the proof produces a strictly positive constant, so the product-of-norms witness is positive. The margin lemma itself only requires L\ge0; its separate m>0 condition does not force L>0. The ReLU in the middle is handled by relu_activation_lipschitz, which is the sharp statement for ReLU: it is exactly 1-Lipschitz in \ell^2, so the activation contributes no looseness at all. Slack can come from bounding each linear layer and from multiplying layerwise constants whose maximizing directions may not align.

The norm slot here is Proofs.tensorL2Norm, the Mathlib-backed real norm from Proofs.Analysis.Lipschitz.Norm, not the Context-dictionary tensorL2Norm from the robustness spec. They agree at \mathbb R, and the predicate takes the norm as a parameter precisely so that a proof may use whichever formulation its lemmas are stated for. Applying a result across the two formulations requires that norm identity.

To use the existential MLP result in a proof, one can unpack its conclusion into a real number, a proof that the number is positive, and a proof of the Lipschitz inequality. Those are three different pieces of information. The inequality can then be applied to any two inputs of shape [inDim]; the hidden dimension constrains the two layer types but disappears from the final input/output predicate. If a deployment needs a numerical radius, the proof must additionally relate the chosen witness to a concrete bound that can be evaluated or certified. Unpacking an existential alone does not print a decimal value for it.

Runtime Margin Reports🔗

The bundled logit-bound report makes the spec-versus-evidence difference visible:

# Read the counts obtained from the bundled logit-bound
# report.
lake exe verify -- margin-report

[margin report] examples=360
[margin report] nominal_ok=349
[margin report] positive_margin=318

nominal_ok counts correctly predicted recorded examples. positive_margin counts entries whose stored bounds imply the required margin. This command checks the report's arithmetic; it does not prove that the stored bounds enclose the model. That stronger claim depends on the verifier that produced the bounds and on a theorem connecting its output to model semantics (Wong and Kolter, 2018). Likewise, the ordering 3.000000\le 3.256617\le 3.741657 above shows why an observed ratio alone cannot supply the upper bound required by a Lipschitz certificate.

Ridge Regression In Binary32🔗

For ridge regression the ideal theorem lives over \mathbb R, while the executable development is in the binary32 ridge-regression implementation, which evaluates the algorithm with FloatLib. The bundled example dataset is x=(1,3), y=(2,4), with \lambda=1 and N=2:

1.166667

1066751317

By hand: \sum x_iy_i=1\cdot2+3\cdot4=14, \sum x_i^2=1+9=10, the denominator is 10+1\cdot2=12, and 14/12=1.1\overline{6}. PyTorch, in float32:

# Check the float32 quotient and inspect its underlying
# integer bit pattern.
xs = torch.tensor([1., 3.]); ys = torch.tensor([2., 4.])
w = (xs @ ys) / (xs @ xs + 1.0 * 2.0)
print(w.item(), w.view(torch.int32).item())

1.1666666269302368 1066751317

The bit patterns are identical: 1066751317 is 0x3F955555 on both sides. Every intermediate here, 14, 10, 12, is exactly representable in binary32, so the only rounding in the whole computation is the final division, and both implementations round it to nearest with ties to even as IEEE 754 requires (Goldberg, 1991). A computation with inexact intermediates would agree only if the two implementations also agreed on association and on intermediate precision, which is exactly the kind of thing our executable model is meant to let us check rather than assume (Boldo and Melquiond, 2011).

What the executable side proves is narrower than the agreement suggests:

@ridgeFit1D_execExpr_toReal_eq_fp32Spec_of_finiteEval : ∀ {n : ℕ}
  (lam :
    ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee
      (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8)
      IEEE32Exec.ExampleIEEE32._proof_1 IEEE32Exec.ExampleIEEE32._proof_2 IEEE32Exec.ExampleIEEE32._proof_3
      IEEE32Exec.ExampleIEEE32._proof_4)
  (S : Dataset (n + 1) IEEE32Exec.ExampleIEEE32) {d : FloatLib.Numerics.Dyadic},
  Floats.IEEE754.IEEE32Exec.FiniteEval (fun x => 0) (ridgeExpr lam S) d →
    (ExecFloat.Binary.toModel (ridgeFit1DExecExpr lam S)).toReal = ridgeFit1DFp32Spec lam S

This theorem concerns ridgeFit1DExecExpr, whose expression tree has its own association. The example above executes the separately defined ordered-fold ridge estimator. No theorem in this module equates those two binary32 evaluation paths for arbitrary data.

This is a finite-evaluation bridge: if the executable expression evaluates without overflowing to infinity or producing a NaN, then its real interpretation agrees with the proof-level FP32 expression. It is not a stability theorem, and it is not an error bound either. What is still missing to connect the two halves of this section is a bound on |\hat w_{\mathrm{fp32}}(S)-\hat w_{\mathbb R}(S)| in terms of the unit roundoff, plus a loss-sensitivity bound that transfers fit error to the compared losses. Both are ordinary numerical analysis; neither is in the file.

The FiniteEval argument in the bridge is evidence about the particular expression ridgeExpr lam S. The variable d records its dyadic result, and the equality then compares two interpretations of that same computation. It does not assert that the equality's right-hand side is the exact real ridge quotient. A later stability transfer would have to control the numerical error for both neighboring datasets, since both fits occur in the loss difference. Keeping track of both executions is essential: bounding the error on the original training set alone leaves the replacement execution uncontrolled.