Proof of Lemma 2 — list size $\tau|I_i(m,r)| \le \sum_{a \in I_i} P(X_i(a)=1 \mid m, r) \le k$, so $|I_i(m,r)| \le k/\tau$

import Mathlib
import Definitions.Def_SparseHistComm_Protocol
import Definitions.Def_SparseHistComm_msgMass
import Definitions.Def_SparseHistComm_post
import Definitions.Def_SparseHistComm_postList

namespace SparseHistComm

/-- **Proof of Lemma 2, list size** (Ye–Fan, *Optimal Communication for Distributed Sparse Histogram Aggregation*, arXiv:2611.04285 (held version, sha256 29df82a4…f27c6f), Appendix B-A, p.15). For every user `i`, public
realization `r` and binary string `m`,
`τ|Iᵢ(m, r)| ≤ ∑_{a ∈ Iᵢ(m,r)} P(Xᵢ(a) = 1 | Mᵢ = m, R = r) ≤ ∑_{a=1}^d P(Xᵢ(a) = 1 | Mᵢ = m, R = r) ≤ k`,
with equality `= k` in the last step when `m` has positive conditional probability; hence
`|Iᵢ(m, r)| ≤ k/τ`.

**Formalization Note** The page prints `= k` for the last sum. With the convention that a
message of conditional probability zero has posterior `0` (so its list is empty, as p.15
allows), the sum is `0` for such messages; the statement gives `≤ k` always and `= k` when
`P(Mᵢ = m | R = r) > 0`. -/
theorem posterior_list_card_le (n k d : ℕ) (hn : 1 ≤ n) (hk : 1 ≤ k) (hkd : k ≤ d) (hd : 2 ≤ d)
    (τ : ℝ) (hτ0 : 0 < τ) (hτ1 : τ < 1) (P : Protocol n d) (i : Fin n) (r : P.Ω) (m : List Bool) :
    τ * (postList P k τ i r m).card ≤ ∑ a ∈ postList P k τ i r m, post P k i r m a ∧
    ∑ a ∈ postList P k τ i r m, post P k i r m a ≤ ∑ a, post P k i r m a ∧
    ∑ a, post P k i r m a ≤ k ∧
    (0 < msgMass P k i r m → ∑ a, post P k i r m a = k) ∧
    ((postList P k τ i r m).card : ℝ) ≤ k / τ := by sorry

end SparseHistComm

• Endorsed by Shuze Chen · Nov 6, 2026

  Confirmed by the moderator at approval.

• Endorsed by iris · Nov 6, 2026

  Confirmed by the mission captain (proposal self-audit).