ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite-range private selection

Example

Let $U$ be a nonempty record universe, let $D$ be its finite-support count databases with add/remove-one-occurrence adjacency, let $R = {a, b}$ , and let $ε > 0$ . The constant utility $u (D, a) = 1$ , $u (D, b) = 0$ has $Δ_{u} = 0$ , so it is inadmissible for the positive-sensitivity exponential mechanism. Fix a possible record $u_{*} \in U$ and define $s (D) = 1$ exactly when $D (u_{*}) > 0$ . Instead set $u (D, a) = 1$ and $u (D, b) = 1 - s (D)$ . Then $Δ_{u} = 1$ , the mechanism is $(ε, 0)$ -differentially private, and it selects $a$ with probability

\frac{e^{ε / 2}}{e^{ε / 2} + e^{ε (1 - s (D)) / 2}} .

Example references

Positive global utility sensitivity

The finite-range mechanism and its normalized weights

Privacy guarantee for the exponential mechanism

Dwork and Roth, The Algorithmic Foundations of Differential Privacy, §3.4, Definition 3.4 and Theorem 3.10, printed pp. 38–39.

Vadhan, The Complexity of Differential Privacy, §4.1, Proposition 4.2.

Facts & Assumptions

Given: A nonempty record universe $U$ , a possible record $u_{*} \in U$ , two candidate outputs $a, b$ , and $ε > 0$ .

[F1]

Database adjacency adds or removes one record occurrence from a finite-support count function.

[F2]

Global utility sensitivity is the attained maximum adjacent score difference over the finite output range.

[F3]

Exponential-mechanism weights are $\exp (ε u (D, r) / (2 Δ_{u}))$ , normalized by their finite positive sum, and require $Δ_{u} > 0$ .

[F4]

Privacy theorem gives $(ε, 0)$ -DP under the stated positive-sensitivity hypotheses.

Verification

1.1F2F3givenalgebra

For the first utility, every score is independent of $D$ , so every adjacent-pair difference is zero and $Δ_{u} = 0$ by [F2]. This fails the positive-sensitivity hypothesis in [F3], so the algorithm is not defined for that utility.

1.2F1F2givenalgebra

For the second utility, adding or removing a record other than $u_{*}$ leaves $s (D)$ unchanged; adding or removing $u_{*}$ changes it by at most one. The empty database and the database with one occurrence of $u_{*}$ are neighbors and change $s$ from zero to one. The score at $a$ is constant, and the score at $b$ changes by exactly the change in $s$ , so the maximum adjacent score difference is attained and equals $Δ_{u} = 1$ .

2.1F3F4step 1.2algebra∎

With $Δ_{u} = 1$ , the weights are $w_{D} (a) = e^{ε / 2}$ and $w_{D} (b) = e^{ε (1 - s (D)) / 2}$ . Normalizing their sum gives the displayed selection probability. Since the range is finite nonempty and the sensitivity is positive, [F4] proves the privacy claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Cynthia Dwork and Aaron Roth, The Algorithmic Foundations of Differential Privacy (standard reference, not scraped)
Salil Vadhan, The Complexity of Differential Privacy, 2017 manuscript (standard reference, not scraped)