When does a Bayesian 95 % credibility interval have 95% coverage? Consider the generative model
$$
\begin{align}
\theta &\sim \pi(\cdot \mid \phi),\\
y \mid \theta &\sim f(\cdot \mid \theta).
\end{align}
$$
Compute the posterior distribution $p(\theta \mid y) \propto f(y \mid \theta) \pi(\theta \mid \phi)$, and define
$$
Q_{y,\phi}(x) = \frac{\int_{-\infty}^x f(y \mid t) \pi(t \mid \phi)\,dt}{\int_{-\infty}^\infty f(y \mid t) \pi(t \mid \phi)\,dt},
$$
as the posterior CDF.
Now, for $0 < \gamma < 1$,  take $I_{\phi, \gamma}(y) = \left(a(y), b(y)\right)$ such that $Q_{y, \phi}(b(y))-Q_{y, \phi}(a(y)) = \gamma$, i.e., $I_{\phi, \gamma}(y)$ is a $\gamma\%$ credibility interval* for $\theta$.

Question: Is it true that
$$
\operatorname{Pr}(\theta \in I_{\phi, \gamma}(y) \mid \theta) \geq \gamma?
$$
In other words, does the $\gamma\%$ credibility interval have $\gamma\%$ coverage when the data are generated according to the model above and the posterior is computed using the same prior $\pi(\cdot \mid \phi)$?

These related questions : q1 and q2 suggest this is true, but I could not for the life of me find a proof. It seems, for instance, that one can show that
$$
\operatorname{Pr}(\theta \in I_{\phi, \gamma}(y) \mid \theta) = \gamma + \epsilon_n,
$$
where $|\epsilon_n| < a/n$ for some $a$.
See page 41 here. I suppose then that it remains to show that for the particular situation of interest here, $\epsilon_n=0$ for all $n$.
*- If you want, you can take the infimum over $b(y)-a(y)$ such that the condition is satisfied, just so that the interval is shortest.
 A: For a given fixed parameter $\theta$, the coverage of a Bayesian credible interval can be greater or lower than the nominal value.
For example, coverage may be greater than nominal if the prior is informative and is centred on the 'true' value of the parameter - see this question and its answers.
Conversely, the coverage can be lower than nominal. For example, if the prior for $\theta$ is uniform on the interval $[0,1]$ and there are no data ($y$ is 'empty') then the coverage might be zero if the true value $\theta<(1-\gamma)/2$ and we always choose the equal-tailed credible interval for $\theta$.
If $\theta$ is not fixed but is instead sampled from the prior then you will get the nominal coverage, as explained in the answers you reference - but this is a somewhat different situation.
A: I like the Wikipedia discussion on this topic, to quote:

Credible intervals are analogous to confidence intervals in frequentist statistics,[2] although they differ on a philosophical basis:[3] Bayesian intervals treat their bounds as fixed and the estimated parameter as a random variable, whereas frequentist confidence intervals treat their bounds as random variables and the parameter as a fixed value...
For example, in an experiment that determines the distribution of possible values of the parameter ${\mu}$, if the subjective probability that ${\mu}$ lies between 35 and 45 is 0.95, then 35 ≤ ${\mu}$ ≤ 45 is a 95% credible interval.

And further as clarification:

Also, Bayesian credible intervals use (and indeed, require) knowledge of the situation-specific prior distribution, while the frequentist confidence intervals do not.

So, to answer the question when does the γ% credibility interval have γ% coverage, likely yes if the sample size that serves as the basis for the prior distribution is very large. While it may still purport to be "subjective probability" based, it likely becomes increasingly indistinguishable from a rounded frequentist estimate. Otherwise, my answer is no.
I would to hear other opinions/arguments, however.
