Does additional data always reduce posterior variance?

This article examines the Bayesian perspective on whether new data always reduces posterior variance. It presents counterexamples using a beta-binomial model where observing a success can increase posterior variance under certain prior conditions (e.g., when prior odds against success are high). It contrasts this with the normal-normal model, where posterior variance always decreases regardless of the observation. The article includes a formal proof in Lean 4 for the beta-binomial case. The content is technical, focusing on statistical theory and mathematical proofs, relevant to data science and machine learning.