clutch.prob.expmech_dp

Headline differential-privacy statement for the discrete exponential mechanism expmech (defined in prob.expmech): "the exponential mechanism is ε-DP". This wraps the per-output ε-DP coupling DPcoupl_expmech into a diffpriv_approx statement (the standard, end-user-facing DP predicate from prob.differential_privacy) via DPcoupl_diffpriv. The adjacency d_scores is a plain R-valued metric on score vectors — no Distance-record axioms are needed: neighbouring score vectors (same length, per-coordinate difference ≤ 1) are at distance 0, everything else at distance 2 > 1. Cost is 2·(num/den) with no additive slack (δ = 0).

Adjacency on score vectors: distance 0 for "1-sensitive neighbours" (same length and per-coordinate difference ≤ 1), distance 2 otherwise. A plain R-valued adjacency — no Distance record needed. The per-coordinate condition is stated over the bounded index range seq 0 (length scores) (via Forall) to keep d_scores *decidable* (the unbounded ∀ k over all of nat is not, a priori). It matches the unbounded ∀ k used by DPcoupl_expmech because scores !!! k for out-of-range k is the inhabitant default 0 on both lists (see adj_bounded_to_unbounded).

Off-range indices read 0 on both lists (total-lookup default), so the bounded per-coordinate bound entails the unbounded one demanded by the coupling lemma DPcoupl_expmech.

The exponential mechanism λ scores, expmech num den scores is (2·Δ·(num/den))-DP (with δ = 0) for the score-vector adjacency d_scores Δ (query sensitivity Δ ≥ 1), whenever the rate is non-negative. With Δ = 1 this recovers the sensitivity-1 statement (2·(num/den))-DP for d_scores 1. Proved by lifting the per-output coupling DPcoupl_expmech through DPcoupl_diffpriv: from d_scores Δ s s' ≤ 1 (so the bool_decide is true, since otherwise the distance would be 2 > 1) we recover the length and per-coordinate conditions that DPcoupl_expmech needs.